Writer Cost Accounting #
This file collects reusable AddWriterT facts for pathwise and expected cost reasoning.
It also equips QueryImpl with additive writer-cost instrumentation.
def
QueryImpl.withAddCost
{ι : Type}
{spec : OracleSpec ι}
{m : Type → Type u_1}
[Monad m]
{ω : Type}
[AddMonoid ω]
(impl : QueryImpl spec m)
(costFn : spec.Domain → ω)
:
QueryImpl spec (AddWriterT ω m)
Instrument an implementation with additive cost accumulation in an AddWriterT layer.
Instances For
def
QueryImpl.withUnitCost
{ι : Type}
{spec : OracleSpec ι}
{m : Type → Type u_1}
[Monad m]
(impl : QueryImpl spec m)
:
QueryImpl spec (AddWriterT ℕ m)
Instrument an implementation with unit additive cost for every query.
Instances For
@[simp]
theorem
QueryImpl.withUnitCost_apply
{ι : Type}
{spec : OracleSpec ι}
{m : Type → Type u_1}
[Monad m]
(impl : QueryImpl spec m)
(t : spec.Domain)
:
def
AddWriterT.PathwiseCostAtMost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
(oa : AddWriterT ω m α)
(w : ω)
:
Pathwise upper bound for an AddWriterT computation: every reachable execution result carries
additive cost at most w.
Instances For
def
AddWriterT.PathwiseCostAtLeast
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
(oa : AddWriterT ω m α)
(w : ω)
:
Pathwise lower bound for an AddWriterT computation: every reachable execution result carries
additive cost at least w.
Instances For
def
AddWriterT.PathwiseCostEqOnSupport
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
(oa : AddWriterT ω m α)
(w : ω)
:
Pathwise exactness on support for an AddWriterT computation: every reachable execution result
carries exactly the additive cost w.
This is the weak extensional notion of pathwise exactness. If oa.run has empty support, it holds
vacuously for every w. Use [AddWriterT.PathwiseHasCost] when the intended meaning is that oa
has an exact pathwise cost and admits at least one reachable execution.
Instances For
@[simp]
theorem
AddWriterT.pathwiseCostEqOnSupport_iff
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
(oa : AddWriterT ω m α)
(w : ω)
:
def
AddWriterT.PathwiseHasCost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
(oa : AddWriterT ω m α)
(w : ω)
:
Pathwise exact cost for an AddWriterT computation: oa has at least one reachable execution,
and every reachable execution result carries exactly the additive cost w.
This is the strong semantic notion of exact cost over execution paths.
Unlike [AddWriterT.HasCost], it does not require cost to be recoverable
from the final output alone. Unlike
[AddWriterT.PathwiseCostEqOnSupport], it is not vacuous on computations with empty support.
Instances For
@[simp]
theorem
AddWriterT.pathwiseHasCost_iff
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
(oa : AddWriterT ω m α)
(w : ω)
:
theorem
AddWriterT.PathwiseHasCost.nonempty
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
(h : oa.PathwiseHasCost w)
:
(support (WriterT.run oa)).Nonempty
theorem
AddWriterT.PathwiseCostEqOnSupport.atMost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
(h : oa.PathwiseCostEqOnSupport w)
:
oa.PathwiseCostAtMost w
theorem
AddWriterT.PathwiseCostEqOnSupport.atLeast
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
(h : oa.PathwiseCostEqOnSupport w)
:
oa.PathwiseCostAtLeast w
theorem
AddWriterT.PathwiseHasCost.eqOnSupport
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
(h : oa.PathwiseHasCost w)
:
theorem
AddWriterT.PathwiseHasCost.atMost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
(h : oa.PathwiseHasCost w)
:
oa.PathwiseCostAtMost w
theorem
AddWriterT.PathwiseHasCost.atLeast
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
(h : oa.PathwiseHasCost w)
:
oa.PathwiseCostAtLeast w
theorem
AddWriterT.PathwiseHasCost.unique
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[PartialOrder ω]
{oa : AddWriterT ω m α}
{w₁ w₂ : ω}
(h₁ : oa.PathwiseHasCost w₁)
(h₂ : oa.PathwiseHasCost w₂)
:
theorem
AddWriterT.pathwiseCostAtMost_of_hasCost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{w b : ω}
(h : oa.HasCost w)
(hwb : w ≤ b)
:
oa.PathwiseCostAtMost b
theorem
AddWriterT.pathwiseCostAtLeast_of_hasCost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddMonoid ω]
[Preorder ω]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{w b : ω}
(h : oa.HasCost w)
(hbw : b ≤ w)
:
oa.PathwiseCostAtLeast b
noncomputable def
AddWriterT.expectedCost
{m : Type → Type u_1}
[Monad m]
{α ω : Type}
[HasEvalSPMF m]
(oa : AddWriterT ω m α)
(val : ω → ENNReal)
:
The expected additive cost of an AddWriterT computation, obtained by taking the expectation
of its cost marginal.
This expectation is computed over the base monad's subdistribution semantics on oa.costs. In
particular, if the underlying computation can fail, the missing mass contributes 0, exactly as
for other wp-style expectations in VCV-io.
Instances For
@[reducible, inline]
noncomputable abbrev
AddWriterT.expectedCostNat
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSPMF m]
(oa : AddWriterT ℕ m α)
:
Convenience specialization of [AddWriterT.expectedCost] to natural-valued additive costs.
Instances For
theorem
AddWriterT.expectedCostNat_eq_tsum_tail_probs
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSPMF m]
(oa : AddWriterT ℕ m α)
:
Tail-sum formula for the natural-valued expected cost of an AddWriterT computation:
E[cost] = ∑ i, Pr[i < cost].
This is the standard discrete expectation identity specialized to the writer-cost marginal.
theorem
AddWriterT.expectedCostNat_le_tsum_of_tail_probs_le
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSPMF m]
(oa : AddWriterT ℕ m α)
{a : ℕ → ENNReal}
(h : ∀ (i : ℕ), (probEvent oa.costs fun (c : ℕ) => i < c) ≤ a i)
:
Tail domination bounds the expected natural-valued writer cost.
If the tail probability Pr[i < cost] is bounded by a i for every i, then
E[cost] ≤ ∑ i, a i.
theorem
AddWriterT.expectedCostNat_eq_sum_tail_probs_of_pathwiseCostAtMost
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSPMF m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(h : oa.PathwiseCostAtMost n)
:
Finite tail-sum formula for natural-valued writer cost under a pathwise upper bound.
If every execution path of oa incurs cost at most n, then the tail probabilities vanish above
n, so the infinite tail sum truncates to Finset.range n.
theorem
AddWriterT.expectedCost_le_of_support_bound
{m : Type → Type u_1}
[Monad m]
{α ω : Type}
[HasEvalSPMF m]
(oa : AddWriterT ω m α)
(val : ω → ENNReal)
(c : ENNReal)
(h : ∀ w ∈ support oa.costs, val w ≤ c)
:
theorem
AddWriterT.expectedCost_le_of_pathwiseCostAtMost
{m : Type → Type u_1}
[Monad m]
{α ω : Type}
[AddMonoid ω]
[HasEvalSPMF m]
[LawfulMonad m]
[Preorder ω]
{oa : AddWriterT ω m α}
{w : ω}
{val : ω → ENNReal}
(h : oa.PathwiseCostAtMost w)
(hval : Monotone val)
:
theorem
AddWriterT.expectedCost_ge_of_pathwiseCostAtLeast
{m : Type → Type u_1}
[Monad m]
{α ω : Type}
[AddMonoid ω]
[LawfulMonad m]
[Preorder ω]
[HasEvalPMF m]
{oa : AddWriterT ω m α}
{w : ω}
{val : ω → ENNReal}
(h : oa.PathwiseCostAtLeast w)
(hval : Monotone val)
:
theorem
AddWriterT.expectedCost_eq_tsum_outputs_of_costsAs
{m : Type → Type u_1}
[Monad m]
{α ω : Type}
[HasEvalSPMF m]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{f : α → ω}
{val : ω → ENNReal}
(h : oa.CostsAs f)
:
theorem
AddWriterT.pathwiseCostAtMost_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : α)
:
(pure x).PathwiseCostAtMost 0
theorem
AddWriterT.pathwiseCostAtLeast_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : α)
:
(pure x).PathwiseCostAtLeast 0
theorem
AddWriterT.pathwiseCostEqOnSupport_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : α)
:
(pure x).PathwiseCostEqOnSupport 0
theorem
AddWriterT.pathwiseHasCost_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : α)
:
(pure x).PathwiseHasCost 0
theorem
AddWriterT.pathwiseCostAtMost_monadLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
:
(monadLift x).PathwiseCostAtMost 0
theorem
AddWriterT.pathwiseCostAtLeast_monadLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
:
(monadLift x).PathwiseCostAtLeast 0
theorem
AddWriterT.pathwiseCostEqOnSupport_monadLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
:
theorem
AddWriterT.pathwiseHasCost_monadLift_of_supportNonempty
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
(hx : (support x).Nonempty)
:
(monadLift x).PathwiseHasCost 0
theorem
AddWriterT.pathwiseCostAtMost_liftM
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
:
(liftM x).PathwiseCostAtMost 0
theorem
AddWriterT.pathwiseCostAtLeast_liftM
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
:
(liftM x).PathwiseCostAtLeast 0
theorem
AddWriterT.pathwiseCostEqOnSupport_liftM
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
:
(liftM x).PathwiseCostEqOnSupport 0
theorem
AddWriterT.pathwiseHasCost_liftM_of_supportNonempty
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(x : m α)
(hx : (support x).Nonempty)
:
(liftM x).PathwiseHasCost 0
theorem
AddWriterT.pathwiseCostAtMost_probCompLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[MonadLiftT ProbComp m]
(x : ProbComp α)
:
(monadLift x).PathwiseCostAtMost 0
theorem
AddWriterT.pathwiseCostAtLeast_probCompLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[MonadLiftT ProbComp m]
(x : ProbComp α)
:
(monadLift x).PathwiseCostAtLeast 0
theorem
AddWriterT.pathwiseCostEqOnSupport_probCompLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[MonadLiftT ProbComp m]
(x : ProbComp α)
:
theorem
AddWriterT.pathwiseHasCost_probCompLift_of_supportNonempty
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[MonadLiftT ProbComp m]
(x : ProbComp α)
(hx : (support (liftM x)).Nonempty)
:
(monadLift x).PathwiseHasCost 0
theorem
AddWriterT.pathwiseCostAtMost_mono
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
{oa : AddWriterT ω m α}
{w₁ w₂ : ω}
(h : oa.PathwiseCostAtMost w₁)
(hw : w₁ ≤ w₂)
:
oa.PathwiseCostAtMost w₂
theorem
AddWriterT.pathwiseCostAtLeast_mono
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
{oa : AddWriterT ω m α}
{w₁ w₂ : ω}
(h : oa.PathwiseCostAtLeast w₂)
(hw : w₁ ≤ w₂)
:
oa.PathwiseCostAtLeast w₁
theorem
AddWriterT.pathwiseCostAtMost_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(w : ω)
:
(addTell w).PathwiseCostAtMost w
theorem
AddWriterT.pathwiseCostAtLeast_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(w : ω)
:
(addTell w).PathwiseCostAtLeast w
theorem
AddWriterT.pathwiseCostEqOnSupport_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(w : ω)
:
theorem
AddWriterT.pathwiseHasCost_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
(w : ω)
:
(addTell w).PathwiseHasCost w
theorem
AddWriterT.pathwiseCostAtMost_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{w : ω}
(f : α → β)
(h : oa.PathwiseCostAtMost w)
:
(f <$> oa).PathwiseCostAtMost w
theorem
AddWriterT.pathwiseCostAtLeast_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{w : ω}
(f : α → β)
(h : oa.PathwiseCostAtLeast w)
:
(f <$> oa).PathwiseCostAtLeast w
theorem
AddWriterT.pathwiseCostEqOnSupport_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{w : ω}
(f : α → β)
(h : oa.PathwiseCostEqOnSupport w)
:
(f <$> oa).PathwiseCostEqOnSupport w
theorem
AddWriterT.pathwiseHasCost_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
{oa : AddWriterT ω m α}
{w : ω}
(f : α → β)
(h : oa.PathwiseHasCost w)
:
(f <$> oa).PathwiseHasCost w
theorem
AddWriterT.pathwiseCostAtMost_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w₁ w₂ : ω}
(h₁ : oa.PathwiseCostAtMost w₁)
(h₂ : ∀ (a : α), (f a).PathwiseCostAtMost w₂)
:
(oa >>= f).PathwiseCostAtMost (w₁ + w₂)
theorem
AddWriterT.pathwiseCostAtLeast_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w₁ w₂ : ω}
(h₁ : oa.PathwiseCostAtLeast w₁)
(h₂ : ∀ (a : α), (f a).PathwiseCostAtLeast w₂)
:
(oa >>= f).PathwiseCostAtLeast (w₁ + w₂)
theorem
AddWriterT.pathwiseCostEqOnSupport_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w₁ w₂ : ω}
(h₁ : oa.PathwiseCostEqOnSupport w₁)
(h₂ : ∀ (a : α), (f a).PathwiseCostEqOnSupport w₂)
:
(oa >>= f).PathwiseCostEqOnSupport (w₁ + w₂)
theorem
AddWriterT.pathwiseHasCost_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w₁ w₂ : ω}
(h₁ : oa.PathwiseHasCost w₁)
(h₂ : ∀ (a : α), (f a).PathwiseHasCost w₂)
:
(oa >>= f).PathwiseHasCost (w₁ + w₂)
theorem
AddWriterT.pathwiseHasCost_bind_zero_left
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w : ω}
(h₁ : oa.PathwiseHasCost 0)
(h₂ : ∀ (a : α), (f a).PathwiseHasCost w)
:
(oa >>= f).PathwiseHasCost w
theorem
AddWriterT.pathwiseHasCost_bind_zero_right
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w : ω}
(h₁ : oa.PathwiseHasCost w)
(h₂ : ∀ (a : α), (f a).PathwiseHasCost 0)
:
(oa >>= f).PathwiseHasCost w
theorem
AddWriterT.pathwiseCostEqOnSupport_bind_zero_left
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w : ω}
(h₁ : oa.PathwiseCostEqOnSupport 0)
(h₂ : ∀ (a : α), (f a).PathwiseCostEqOnSupport w)
:
(oa >>= f).PathwiseCostEqOnSupport w
theorem
AddWriterT.pathwiseCostEqOnSupport_bind_zero_right
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{oa : AddWriterT ω m α}
{f : α → AddWriterT ω m β}
{w : ω}
(h₁ : oa.PathwiseCostEqOnSupport w)
(h₂ : ∀ (a : α), (f a).PathwiseCostEqOnSupport 0)
:
(oa >>= f).PathwiseCostEqOnSupport w
theorem
AddWriterT.pathwiseCostAtMost_fin_mOfFn
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{n : ℕ}
{k : ω}
{f : Fin n → AddWriterT ω m α}
(h : ∀ (i : Fin n), (f i).PathwiseCostAtMost k)
:
(Fin.mOfFn n f).PathwiseCostAtMost (n • k)
theorem
AddWriterT.pathwiseCostAtLeast_fin_mOfFn
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{n : ℕ}
{k : ω}
{f : Fin n → AddWriterT ω m α}
(h : ∀ (i : Fin n), (f i).PathwiseCostAtLeast k)
:
(Fin.mOfFn n f).PathwiseCostAtLeast (n • k)
theorem
AddWriterT.pathwiseHasCost_fin_mOfFn
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{ω : Type}
[AddCommMonoid ω]
[PartialOrder ω]
[LawfulMonad m]
[IsOrderedAddMonoid ω]
{n : ℕ}
{k : ω}
{f : Fin n → AddWriterT ω m α}
(h : ∀ (i : Fin n), (f i).PathwiseHasCost k)
:
(Fin.mOfFn n f).PathwiseHasCost (n • k)
def
AddWriterT.QueryBoundedAboveBy
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
(oa : AddWriterT ℕ m α)
(n : ℕ)
:
Pathwise upper bound for a unit-cost AddWriterT computation.
Instances For
def
AddWriterT.QueryBoundedBelowBy
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
(oa : AddWriterT ℕ m α)
(n : ℕ)
:
Pathwise lower bound for a unit-cost AddWriterT computation.
Instances For
theorem
AddWriterT.queryBoundedAboveBy_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
(x : α)
:
(pure x).QueryBoundedAboveBy 0
theorem
AddWriterT.queryBoundedBelowBy_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
(x : α)
:
(pure x).QueryBoundedBelowBy 0
theorem
AddWriterT.queryBoundedAboveBy_monadLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
(x : m α)
:
(monadLift x).QueryBoundedAboveBy 0
theorem
AddWriterT.queryBoundedBelowBy_monadLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
(x : m α)
:
(monadLift x).QueryBoundedBelowBy 0
theorem
AddWriterT.queryBoundedAboveBy_mono
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{oa : AddWriterT ℕ m α}
{n₁ n₂ : ℕ}
(h : oa.QueryBoundedAboveBy n₁)
(hn : n₁ ≤ n₂)
:
oa.QueryBoundedAboveBy n₂
theorem
AddWriterT.queryBoundedBelowBy_mono
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{oa : AddWriterT ℕ m α}
{n₁ n₂ : ℕ}
(h : oa.QueryBoundedBelowBy n₂)
(hn : n₁ ≤ n₂)
:
oa.QueryBoundedBelowBy n₁
theorem
AddWriterT.queryBoundedAboveBy_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
[LawfulMonad m]
(w : ℕ)
:
(addTell w).QueryBoundedAboveBy w
theorem
AddWriterT.queryBoundedBelowBy_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
[LawfulMonad m]
(w : ℕ)
:
(addTell w).QueryBoundedBelowBy w
theorem
AddWriterT.queryBoundedAboveBy_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(f : α → β)
(h : oa.QueryBoundedAboveBy n)
:
(f <$> oa).QueryBoundedAboveBy n
theorem
AddWriterT.queryBoundedBelowBy_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(f : α → β)
(h : oa.QueryBoundedBelowBy n)
:
(f <$> oa).QueryBoundedBelowBy n
theorem
AddWriterT.queryBoundedAboveBy_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{f : α → AddWriterT ℕ m β}
{n₁ n₂ : ℕ}
(h₁ : oa.QueryBoundedAboveBy n₁)
(h₂ : ∀ (a : α), (f a).QueryBoundedAboveBy n₂)
:
(oa >>= f).QueryBoundedAboveBy (n₁ + n₂)
theorem
AddWriterT.queryBoundedBelowBy_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{f : α → AddWriterT ℕ m β}
{n₁ n₂ : ℕ}
(h₁ : oa.QueryBoundedBelowBy n₁)
(h₂ : ∀ (a : α), (f a).QueryBoundedBelowBy n₂)
:
(oa >>= f).QueryBoundedBelowBy (n₁ + n₂)
theorem
AddWriterT.queryBoundedAboveBy_fin_mOfFn
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
{n k : ℕ}
{f : Fin n → AddWriterT ℕ m α}
(h : ∀ (i : Fin n), (f i).QueryBoundedAboveBy k)
:
(Fin.mOfFn n f).QueryBoundedAboveBy (n * k)
theorem
AddWriterT.queryBoundedBelowBy_fin_mOfFn
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
{n k : ℕ}
{f : Fin n → AddWriterT ℕ m α}
(h : ∀ (i : Fin n), (f i).QueryBoundedBelowBy k)
:
(Fin.mOfFn n f).QueryBoundedBelowBy (n * k)
def
AddWriterT.QueryCostExactly
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
(oa : AddWriterT ℕ m α)
(n : ℕ)
:
Pathwise exact cost for a unit-cost AddWriterT computation: every reachable execution
carries exactly n unit queries.
Instances For
theorem
AddWriterT.QueryCostExactly.toAbove
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(h : oa.QueryCostExactly n)
:
oa.QueryBoundedAboveBy n
theorem
AddWriterT.QueryCostExactly.toBelow
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(h : oa.QueryCostExactly n)
:
oa.QueryBoundedBelowBy n
theorem
AddWriterT.queryCostExactly_pure
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
(x : α)
:
(pure x).QueryCostExactly 0
theorem
AddWriterT.queryCostExactly_monadLift
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
(x : m α)
:
(monadLift x).QueryCostExactly 0
theorem
AddWriterT.queryCostExactly_addTell
{m : Type → Type u_1}
[Monad m]
[HasEvalSet m]
[LawfulMonad m]
(w : ℕ)
:
(addTell w).QueryCostExactly w
theorem
AddWriterT.queryCostExactly_map
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(f : α → β)
(h : oa.QueryCostExactly n)
:
(f <$> oa).QueryCostExactly n
theorem
AddWriterT.queryCostExactly_bind
{m : Type → Type u_1}
[Monad m]
{α β : Type}
[HasEvalSet m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{f : α → AddWriterT ℕ m β}
{n₁ n₂ : ℕ}
(h₁ : oa.QueryCostExactly n₁)
(h₂ : ∀ (a : α), (f a).QueryCostExactly n₂)
:
(oa >>= f).QueryCostExactly (n₁ + n₂)
theorem
AddWriterT.queryCostExactly_fin_mOfFn
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSet m]
[LawfulMonad m]
{n k : ℕ}
{f : Fin n → AddWriterT ℕ m α}
(h : ∀ (i : Fin n), (f i).QueryCostExactly k)
:
(Fin.mOfFn n f).QueryCostExactly (n * k)
theorem
AddWriterT.expectedCostNat_le_of_queryBoundedAboveBy
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalSPMF m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(h : oa.QueryBoundedAboveBy n)
:
theorem
AddWriterT.expectedCostNat_ge_of_queryBoundedBelowBy
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalPMF m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(h : oa.QueryBoundedBelowBy n)
:
theorem
AddWriterT.expectedCostNat_eq_of_queryCostExactly
{m : Type → Type u_1}
[Monad m]
{α : Type}
[HasEvalPMF m]
[LawfulMonad m]
{oa : AddWriterT ℕ m α}
{n : ℕ}
(h : oa.QueryCostExactly n)
: