Evaluation Distributions of Computations with Bind #
File for lemmas about evalDist and support involving the monadic pure and bind.
@[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 : α)
:
@[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_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 : α)
:
@[simp]
theorem
support_bind
{α β : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SetM]
[LawfulMonadLiftT m SetM]
(mx : m α)
(my : α → m β)
:
@[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
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
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
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
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
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
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
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_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.
theorem
probEvent_bind_bind_swap
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[LawfulMonad m]
(mx : m α)
(my : m β)
(f : α → β → m γ)
(q : γ → Prop)
:
Swapping two independent random draws preserves probability of any event.
theorem
probOutput_bind_bind_swap
{α β γ : Type u}
{m : Type u → Type v}
[Monad m]
[MonadLiftT m SPMF]
[LawfulMonadLiftT m SPMF]
[LawfulMonad m]
(mx : m α)
(my : m β)
(f : α → β → m γ)
(z : γ)
:
Swapping two independent random draws preserves the probability of any fixed output.
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.