Evaluation Distributions of Computations with Bind #
File for lemmas about evalSPMF and support involving the monadic pure and bind.
Probabilities of pure #
theorem
evalSPMF_pure
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
{α : Type u}
(x : α)
:
@[simp]
theorem
evalSPMF_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 #
theorem
evalSPMF_bind_of_support_eq_empty
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
(mx : m α)
(my : α → m β)
(h : support mx = ∅)
:
theorem
probOutput_bind_eq_expectedValue
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(mx : m α)
(my : α → m β)
(y : β)
:
probOutput_bind_eq_tsum with the sum packaged as an expectedValue, the head gcongr
descends through.
theorem
probEvent_bind_eq_expectedValue
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
(mx : m α)
(my : α → m β)
(q : β → Prop)
:
probEvent_bind_eq_tsum with the sum packaged as an expectedValue.
theorem
probOutput_bind_eq_tsum_subtype
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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_mul
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{q : β → Prop}
{p : α → Prop}
{ε : ENNReal}
(hle : ∀ x ∈ support mx, p x → probEvent (my x) q ≤ ε)
(hzero : ∀ x ∈ support mx, ¬p x → probEvent (my x) q = 0)
:
If a continuation event is bounded by ε exactly on a prefix event and is
impossible off that event, then only the prefix mass is charged.
theorem
probEvent_bind_le_probEvent_div
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{my : α → m β}
{q : β → Prop}
{p : α → Prop}
{c : ENNReal}
(hle : ∀ x ∈ support mx, p x → probEvent (my x) q ≤ c⁻¹)
(hzero : ∀ x ∈ support mx, ¬p x → probEvent (my x) q = 0)
:
Division-form corollary of probEvent_bind_le_probEvent_mul.
theorem
probEvent_le_add_of_imp_or
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{p q r : α → Prop}
(h : ∀ x ∈ support mx, p x → q x ∨ r x)
:
Partition an event pointwise into a main event and an exceptional event.
theorem
probEvent_bind_le_probEvent_convex
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[EvalDistCompatible m]
[HasEvalFinset m]
(mx : m α)
(my : α → m β)
[DecidableEq α]
(q : β → Prop)
:
theorem
support_bind_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
[MonadAttach m]
[ExactMonadAttach m]
(mx : m α)
(my : m β)
:
theorem
finSupport_bind_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
[MonadAttach m]
[ExactMonadAttach m]
[HasEvalFinset m]
[DecidableEq β]
[DecidableEq α]
(mx : m α)
(my : m β)
:
instance
instLawfulEvalDistSemanticsOfMonadLiftTSPMF
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
:
The compatibility adapter satisfies the Giry pure/bind laws for every lawful SPMF
lift, so the 𝒟-level laws (evalDist_pure, evalDist_bind, evalDist_map, …) hold with no
measure specification in scope.
@[simp]
theorem
probOutput_bind_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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.
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]
[MonadAttach m]
[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
probOutput_bind_congr
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{y : β}
(h : ∀ x ∈ support mx, 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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[EvalDistCompatible m]
(mx : m α)
{ob₁ ob₂ : α → m β}
(q : β → Prop)
(h : ∀ (x : α), probEvent (ob₁ x) q = probEvent (ob₂ x) q)
:
theorem
evalSPMF_bind_congr
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
(h : ∀ x ∈ support mx, 𝒮[ob₁ x] = 𝒮[ob₂ x])
:
theorem
evalSPMF_bind_congr'
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{my oc : α → m β}
{q : β → Prop}
(h : ∀ x ∈ support mx, probEvent (my x) q ≤ probEvent (oc x) q)
:
theorem
probOutput_bind_mono_div_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{y : β}
{r : ENNReal}
(h : ∀ x ∈ support mx, Pr[= y | ob₁ x] ≤ Pr[= y | ob₂ x] / r)
:
Pointwise division bounds on bind continuations factor through the bind.
theorem
probEvent_bind_mono_div_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[EvalDistCompatible m]
{mx : m α}
{ob₁ ob₂ : α → m β}
{q : β → Prop}
{r : ENNReal}
(h : ∀ x ∈ support mx, probEvent (ob₁ x) q ≤ probEvent (ob₂ x) q / r)
:
Event form of probOutput_bind_mono_div_const.
theorem
probOutput_bind_congr_div_const
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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]
[MonadAttach m]
[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_le_probEvent_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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_congr_le_add
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[MonadAttach m]
[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
evalSPMF_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
evalSPMF_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 evalSPMF_bind_bind_swap.
Complement bounds #
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_finsetSum
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
{ι' : Type u_1}
(mx : m α)
(s : Finset ι')
(f : ι' → α → ENNReal)
:
A finite sum inside an expectation may be taken outside: linearity of expectation over a
Finset of summands.
theorem
tsum_probOutput_mul_of_const_on_support
{α : Type u}
{m : Type u → Type v}
[MonadLiftT m SPMF]
[MonadAttach m]
[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.