Evaluation Distributions of Computations with Bind #
File for lemmas about evalDist and support involving the monadic pure and bind.
Probabilities of pure #
@[simp]
theorem
support_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(x : α)
:
theorem
mem_support_pure_iff
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(x y : α)
:
theorem
mem_support_pure_iff'
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(x y : α)
:
theorem
eq_of_mem_support_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
{x y : α}
(h : y ∈ support (pure x))
:
obtain-friendly forward direction of mem_support_pure_iff: membership in the support
of a pure forces equality with the pure value.
@[simp]
theorem
finSupport_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
[HasEvalFinset m]
[DecidableEq α]
(x : α)
:
theorem
mem_finSupport_pure_iff
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
[HasEvalFinset m]
[DecidableEq α]
(x y : α)
:
theorem
mem_finSupport_pure_iff'
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
[HasEvalFinset m]
[DecidableEq α]
(x y : α)
:
@[simp]
theorem
evalDist_pure
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
{α : Type u}
(x : α)
:
@[simp]
theorem
evalDist_comp_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
:
@[simp]
theorem
probOutput_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[DecidableEq α]
(x y : α)
:
@[simp]
theorem
probOutput_pure_self
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(x : α)
:
theorem
probOutput_pure_bool_le_or
{m : Type → Type}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(win inner outer : Bool)
(h : win = true → inner = true ∨ outer = true)
:
Boolean monotonicity of pure outcome probability into a disjunction: if win implies
inner ∨ outer, then the probability of outcome true under pure win is bounded by the sum of
the probabilities under pure inner and pure outer.
theorem
probOutput_pure_bool_le
{m : Type → Type}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(b₁ b₂ : Bool)
(h : b₁ = true → b₂ = true)
:
Boolean monotonicity of pure outcome probability: if b₁ implies b₂, then the probability
of outcome true under pure b₁ is bounded by that under pure b₂.
theorem
probOutput_pure_eq_indicator
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(x y : α)
:
Fallback when we don't have decidable equality.
@[simp]
theorem
probEvent_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(x : α)
(p : α → Prop)
[DecidablePred p]
:
theorem
probEvent_pure_eq_indicator
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(x : α)
(p : α → Prop)
:
Fallback when we don't have decidable equality.
@[simp]
theorem
probFailure_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(x : α)
:
Probabilities of bind #
@[simp]
theorem
support_bind
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(mx : m α)
(my : α → m β)
:
theorem
support_bind_exists
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
{x : m α}
{f : α → m β}
{y : β}
(hy : y ∈ support (x >>= f))
:
obtain-friendly forward direction of mem_support_bind_iff: peel an element of the
support of a bind into a witness for the first computation and membership for the second.
@[simp]
theorem
finSupport_bind
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
[HasEvalFinset m]
[DecidableEq α]
[DecidableEq β]
(mx : m α)
(my : α → m β)
:
theorem
mem_finSupport_bind_iff
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
[HasEvalFinset m]
[DecidableEq α]
[DecidableEq β]
(mx : m α)
(my : α → m β)
(y : β)
:
theorem
evalDist_bind_of_support_eq_empty
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
(my : α → m β)
(h : support mx = ∅)
:
theorem
probOutput_bind_eq_tsum_subtype
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
(my : α → m β)
(y : β)
:
Version of probOutput_bind_eq_tsum that sums only over the subtype given by the support
of the first computation. This can be useful to avoid looking at edge cases that can't actually
happen in practice after the first computation. A common example is if the first computation
does some error handling to avoids returning malformed outputs.
theorem
probEvent_bind_eq_tsum_subtype
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
(my : α → m β)
(q : β → Prop)
:
theorem
probEvent_bind_le_of_forall_le
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{q : β → Prop}
{ε : ENNReal}
(h : ∀ x ∈ support mx, probEvent (my x) q ≤ ε)
:
If Pr[q | my x] ≤ ε for every x in the support of mx, then the bound also
holds for the bind.
theorem
probEvent_bind_le_probEvent
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{q : β → Prop}
{p : α → Prop}
(h : ∀ x ∈ support mx, ¬p x → probEvent (my x) q = 0)
:
If the continuation can satisfy q only after a support point satisfying p,
then the probability of q after the bind is at most the probability of p in
the prefix computation.
theorem
probEvent_bind_le_probEvent_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{q : β → Prop}
{p : α → Prop}
{ε : ENNReal}
(h : ∀ x ∈ support mx, ¬p x → probEvent (my x) q ≤ ε)
:
Prefix-event split for a bind. Prefix points satisfying p are charged in
full; off-prefix continuations are charged by the uniform tail bound ε.
theorem
probEvent_bind_le_probEvent_convex
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{q : β → Prop}
{p : α → Prop}
{ε : ENNReal}
(h : ∀ x ∈ support mx, ¬p x → probEvent (my x) q ≤ ε)
:
Convex prefix-event split for a bind. The off-prefix tail bound ε is charged
only on the mass outside p, giving Pr[p] + (1 - Pr[p]) * ε.
theorem
probOutput_bind_eq_sum_finSupport
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
[HasEvalFinset m]
(mx : m α)
(my : α → m β)
[DecidableEq α]
(y : β)
:
theorem
probEvent_bind_eq_sum_finSupport
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
[HasEvalFinset m]
(mx : m α)
(my : α → m β)
[DecidableEq α]
(q : β → Prop)
:
@[simp]
theorem
finSupport_bind_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
[HasEvalFinset m]
[DecidableEq β]
[DecidableEq α]
(mx : m α)
(my : m β)
:
theorem
probOutput_bind_of_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{my : α → m β}
{y : β}
{r : ENNReal}
(h : ∀ x ∈ support mx, Pr[= y | my x] = r)
:
@[simp]
theorem
probOutput_bind_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
(my : m β)
(y : β)
:
theorem
probEvent_bind_of_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{my : α → m β}
{p : β → Prop}
{r : ENNReal}
(h : ∀ x ∈ support mx, probEvent (my x) p = r)
:
@[simp]
theorem
probEvent_bind_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
(my : m β)
(p : β → Prop)
:
theorem
probFailure_bind_of_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{r : ENNReal}
(h : ∀ x ∈ support mx, Pr[⊥ | my x] = r)
:
Write the probability of mx >>= my failing given that my has constant failure chance over
the possible outputs in support mx as a fixed expression without any sums.
theorem
probFailure_bind_of_const'
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{r : ENNReal}
(hr : r ≠ ⊤)
(h : ∀ x ∈ support mx, Pr[⊥ | my x] = r)
:
theorem
probFailure_bind_eq_sub_mul
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
(my : α → m β)
(r : ENNReal)
(hr : r ≠ ⊤)
(h : ∀ x ∈ support mx, Pr[⊥ | my x] = r)
:
theorem
probFailure_bind_le_add_of_forall
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{r : ENNReal}
(hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r)
:
theorem
probFailure_bind_le_of_forall'
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{s : ENNReal}
(h' : Pr[⊥ | mx] = s)
(my : α → m β)
{r : ENNReal}
(hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r)
:
Version of probFailure_bind_le_of_forall with that allows a manual Pr[⊥ | mx] value.
theorem
probFailure_bind_le_of_forall
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
(h' : Pr[⊥ | mx] = 0)
{my : α → m β}
{r : ENNReal}
(hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r)
:
Version of probFailure_bind_le_of_forall when mx never fails.
@[simp]
theorem
allOutputsSatisfy_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(p : α → Prop)
(x : α)
:
@[simp]
theorem
someOutputSatisfies_pure
{α : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(p : α → Prop)
(x : α)
:
@[simp]
theorem
allOutputsSatisfy_bind
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(mx : m α)
(my : α → m β)
(p : β → Prop)
:
@[simp]
theorem
someOutputSatisfies_bind
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(mx : m α)
(my : α → m β)
(p : β → Prop)
:
someOutputSatisfies p (mx >>= my) ↔ someOutputSatisfies (fun (a : α) => someOutputSatisfies p (my a)) mx
Congruence and monotonicity for bind #
theorem
mul_le_probEvent_bind
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{p : α → Prop}
{q : β → Prop}
{r r' : ENNReal}
(h : r ≤ probEvent mx p)
(h' : ∀ x ∈ support mx, p x → r' ≤ probEvent (my x) q)
:
theorem
probFailure_bind_congr
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{my : α → m β}
{oc : α → m γ}
(h : ∀ x ∈ support mx, Pr[⊥ | my x] = Pr[⊥ | oc x])
:
theorem
probOutput_bind_congr
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{y : β}
(h : ∀ x ∈ support mx, Pr[= y | ob₁ x] = Pr[= y | ob₂ x])
:
theorem
probOutput_bind_congr'
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{ob₁ ob₂ : α → m β}
(y : β)
(h : ∀ (x : α), Pr[= y | ob₁ x] = Pr[= y | ob₂ x])
:
theorem
probOutput_bind_mono
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{oc : α → m γ}
{y : β}
{z : γ}
(h : ∀ x ∈ support mx, Pr[= y | my x] ≤ Pr[= z | oc x])
:
theorem
probEvent_bind_congr
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{q : β → Prop}
(h : ∀ x ∈ support mx, probEvent (ob₁ x) q = probEvent (ob₂ x) q)
:
theorem
probEvent_bind_congr'
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{ob₁ ob₂ : α → m β}
(q : β → Prop)
(h : ∀ (x : α), probEvent (ob₁ x) q = probEvent (ob₂ x) q)
:
theorem
evalDist_bind_congr'
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{ob₁ ob₂ : α → m β}
(h : ∀ (x : α), 𝒟[ob₁ x] = 𝒟[ob₂ x])
:
theorem
probEvent_bind_mono
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my oc : α → m β}
{q : β → Prop}
(h : ∀ x ∈ support mx, probEvent (my x) q ≤ probEvent (oc x) q)
:
theorem
probOutput_bind_congr_div_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{y : β}
{r : ENNReal}
(h : ∀ x ∈ support mx, Pr[= y | ob₁ x] = Pr[= y | ob₂ x] / r)
:
theorem
probEvent_bind_congr_div_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{q : β → Prop}
{r : ENNReal}
(h : ∀ x ∈ support mx, probEvent (ob₁ x) q = probEvent (ob₂ x) q / r)
:
theorem
probOutput_bind_congr_eq_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{y : β}
{z₁ : γ₁}
{z₂ : γ₂}
(h : ∀ x ∈ support mx, Pr[= y | my x] = Pr[= z₁ | oc₁ x] + Pr[= z₂ | oc₂ x])
:
theorem
probEvent_bind_congr_eq_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{q : β → Prop}
{q₁ : γ₁ → Prop}
{q₂ : γ₂ → Prop}
(h : ∀ x ∈ support mx, probEvent (my x) q = probEvent (oc₁ x) q₁ + probEvent (oc₂ x) q₂)
:
theorem
probOutput_bind_congr_le_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{y : β}
{z₁ : γ₁}
{z₂ : γ₂}
(h : ∀ x ∈ support mx, Pr[= y | my x] ≤ Pr[= z₁ | oc₁ x] + Pr[= z₂ | oc₂ x])
:
theorem
probOutput_bind_congr_add_le
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{y : β}
{z₁ : γ₁}
{z₂ : γ₂}
(h : ∀ x ∈ support mx, Pr[= z₁ | oc₁ x] + Pr[= z₂ | oc₂ x] ≤ Pr[= y | my x])
:
theorem
probEvent_bind_congr_add_le
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{q : β → Prop}
{q₁ : γ₁ → Prop}
{q₂ : γ₂ → Prop}
(h : ∀ x ∈ support mx, probEvent (oc₁ x) q₁ + probEvent (oc₂ x) q₂ ≤ probEvent (my x) q)
:
theorem
probOutput_bind_congr_le_sub
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{y : β}
{z₁ : γ₁}
{z₂ : γ₂}
(h : ∀ x ∈ support mx, Pr[= y | my x] ≤ Pr[= z₁ | oc₁ x] - Pr[= z₂ | oc₂ x])
(h' : ∀ x ∈ support mx, Pr[= z₂ | oc₂ x] ≤ Pr[= z₁ | oc₁ x])
:
theorem
probEvent_bind_congr_le_sub
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{q : β → Prop}
{q₁ : γ₁ → Prop}
{q₂ : γ₂ → Prop}
(h : ∀ x ∈ support mx, probEvent (my x) q ≤ probEvent (oc₁ x) q₁ - probEvent (oc₂ x) q₂)
(h' : ∀ x ∈ support mx, probEvent (oc₂ x) q₂ ≤ probEvent (oc₁ x) q₁)
:
theorem
probOutput_bind_congr_sub_le
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{y : β}
{z₁ : γ₁}
{z₂ : γ₂}
(h : ∀ x ∈ support mx, Pr[= z₁ | oc₁ x] - Pr[= z₂ | oc₂ x] ≤ Pr[= y | my x])
:
theorem
probEvent_bind_congr_sub_le
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{γ₁ γ₂ : Type u}
{mx : m α}
{my : α → m β}
{oc₁ : α → m γ₁}
{oc₂ : α → m γ₂}
{q : β → Prop}
{q₁ : γ₁ → Prop}
{q₂ : γ₂ → Prop}
(h : ∀ x ∈ support mx, probEvent (oc₁ x) q₁ - probEvent (oc₂ x) q₂ ≤ probEvent (my x) q)
:
theorem
probEvent_bind_le_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{p : α → Prop}
{q : β → Prop}
{ε₁ ε₂ : ENNReal}
(h₁ : (probEvent mx fun (x : α) => ¬p x) ≤ ε₁)
(h₂ : ∀ x ∈ support mx, p x → (probEvent (my x) fun (y : β) => ¬q y) ≤ ε₂)
:
Union bound for bind: if Pr[ ¬p | mx] ≤ ε₁ and Pr[ ¬q | my x] ≤ ε₂ for all x satisfying
p, then Pr[ ¬q | mx >>= my] ≤ ε₁ + ε₂. Useful for sequential composition of error bounds.
theorem
probEvent_bind_congr_le_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
{mx : m α}
{my oc : α → m β}
{q : β → Prop}
{ε : ENNReal}
(h : ∀ x ∈ support mx, probEvent (my x) q ≤ probEvent (oc x) q + ε)
:
probEvent version of probEvent_bind_mono with additive error bound.
Swapping independent draws #
theorem
evalDist_bind_bind_swap
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(mx : m α)
(my : m β)
(f : α → β → m γ)
:
Swapping two independent random draws preserves the output distribution: although
mx >>= fun a => my >>= fun b => f a b and my >>= fun b => mx >>= fun a => f a b need not be
equal as m-computations when m is non-commutative, the two draws are independent, so their
output distributions agree. The probEvent/probOutput forms (probEvent_bind_bind_swap,
probOutput_bind_bind_swap) are corollaries.
theorem
probEvent_bind_bind_swap
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(mx : m α)
(my : m β)
(f : α → β → m γ)
(q : γ → Prop)
:
Swapping two independent random draws preserves probability of any event. Corollary of
evalDist_bind_bind_swap.
theorem
probOutput_bind_bind_swap
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(mx : m α)
(my : m β)
(f : α → β → m γ)
(z : γ)
:
Swapping two independent random draws preserves the probability of any fixed output. Corollary
of evalDist_bind_bind_swap.
Complement bounds #
@[deprecated probEvent_compl_le_of_one_sub_le (since := "2026-06-25")]
theorem
probEvent_compl_le_of_ge
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
{mx : m α}
{p : α → Prop}
{ε : ENNReal}
(hfail : Pr[⊥ | mx] = 0)
(h : 1 - ε ≤ probEvent mx p)
:
Alias of probEvent_compl_le_of_one_sub_le.
If 1 - ε ≤ Pr[ p | mx] and mx never fails, then Pr[ ¬p | mx] ≤ ε.
@[deprecated probEvent_one_sub_le_of_compl_le (since := "2026-06-25")]
theorem
probEvent_ge_of_compl_le
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
{mx : m α}
{p : α → Prop}
{ε : ENNReal}
(hfail : Pr[⊥ | mx] = 0)
(h : (probEvent mx fun (x : α) => ¬p x) ≤ ε)
:
Alias of probEvent_one_sub_le_of_compl_le.
If Pr[ ¬p | mx] ≤ ε and mx never fails, then 1 - ε ≤ Pr[ p | mx].
Union bounds #
theorem
probEvent_exists_finset_le_sum
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
{ι : Type u_1}
(s : Finset ι)
(mx : m α)
(E : ι → α → Prop)
:
Union bound for finset-indexed events: the probability that some event in s holds
is at most the sum of the individual event probabilities.
Expectation algebra for nonnegative functionals #
theorem
tsum_probOutput_bind_mul
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(mx : m α)
(g : α → m β)
(f : β → ENNReal)
:
Tonelli-style rearrangement: the expectation of a nonnegative functional under a
bind is the outer expectation of the inner expectations.
theorem
tsum_probOutput_map_mul
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[LawfulMonad m]
(mx : m α)
(f : α → β)
(g : β → ENNReal)
:
Expectation of a nonnegative functional under a Functor.map: the functional is
precomposed with the map.
theorem
tsum_probOutput_mul_of_const_on_support
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
[MonadLiftT m SetM]
[EvalDistCompatible m]
(mx : m α)
{c : ENNReal}
{F : α → ENNReal}
(hconst : ∀ z ∈ support mx, F z = c)
(hmass : Pr[⊥ | mx] = 0)
:
The expectation of a nonnegative functional F that is constant (equal to c) on the
support of a never-failing (sub)probability computation equals c.