Probability bounds for computation observations

Union bounds, event splitting, and conditioning on a common draw are stated for events observed in Prop, so intermediate types need no measurable-space arguments in the public statements. The common draw may lose mass; lower bounds ask for its losslessness as the trivially true event. Bounds that only need to hold on structurally reachable outputs go through core attachment. Conditional independent draws bound the squared probability of a single event.

theorem prEvent_bind_sq_le_bind_pair {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (source : m α) (f : α → m β) (p : β → Prop) : 𝒟[do let y ← source >>= f pure (p y)] {True} ^ 2 ≤ 𝒟[do let x ← source let a ← f x let b ← f x pure (p a ∧ p b)] {True}

Two independent executions after a common draw bound the squared single-execution event.

theorem sum_prEvent_option_map_eq_some_le_isSome {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α γ : Type} [Fintype γ] (mx : m (Option α)) (select : α → Option γ) : ∑ k : γ, 𝒟[do let r ← mx pure (Option.map select r = some (some k))] {True} ≤ 𝒟[do let r ← mx pure (r.isSome = true)] {True}

Finite selector events in an optional output have total probability at most the event that an output is present. Intermediate values need no measurable-space argument.

Event algebra and union bounds

theorem prEvent_or_le {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) : 𝒟[do let x ← mx pure (p x ∨ q x)] {True} ≤ 𝒟[do let x ← mx pure (p x)] {True} + 𝒟[do let x ← mx pure (q x)] {True}

Union bound for two events after a common draw.

theorem prEvent_exists_finset_le {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α ι : Type} (s : Finset ι) (mx : m α) (p : ι → α → Prop) : 𝒟[do let x ← mx pure (∃ i ∈ s, p i x)] {True} ≤ ∑ i ∈ s, 𝒟[do let x ← mx pure (p i x)] {True}

Union bound over a finite index set.

theorem prEvent_exists_le {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α ι : Type} [Fintype ι] (mx : m α) (p : ι → α → Prop) : 𝒟[do let x ← mx pure (∃ (i : ι), p i x)] {True} ≤ ∑ i : ι, 𝒟[do let x ← mx pure (p i x)] {True}

Union bound over a finite type.

theorem prEvent_exists_le_card_mul {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α ι : Type} [Fintype ι] (mx : m α) (p : ι → α → Prop) {ε : ENNReal} (h : ∀ (i : ι), 𝒟[do let x ← mx pure (p i x)] {True} ≤ ε) : 𝒟[do let x ← mx pure (∃ (i : ι), p i x)] {True} ≤ ↑(Fintype.card ι) * ε

A uniform bound on each of finitely many events bounds their union by the count.

theorem prEvent_eq_prEvent_and_add_prEvent_and_not {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[do let x ← mx pure (p x ∧ q x)] {True} + 𝒟[do let x ← mx pure (p x ∧ ¬q x)] {True}

An event splits along a second predicate.

theorem prEvent_le_prEvent_add_prEvent_and_not {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} ≤ 𝒟[do let x ← mx pure (q x)] {True} + 𝒟[do let x ← mx pure (p x ∧ ¬q x)] {True}

An event is bounded by a second one plus the part outside it.

theorem prEvent_and_le_left {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) : 𝒟[do let x ← mx pure (p x ∧ q x)] {True} ≤ 𝒟[do let x ← mx pure (p x)] {True}

A conjunction is bounded by its first conjunct.

theorem prEvent_and_le_right {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) : 𝒟[do let x ← mx pure (p x ∧ q x)] {True} ≤ 𝒟[do let x ← mx pure (q x)] {True}

A conjunction is bounded by its second conjunct.

Conditioning on a common draw

theorem prEvent_bind_le_of_forall_le {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (f : α → m β) (q : β → Prop) {ε : ENNReal} (h : ∀ (a : α), 𝒟[do let y ← f a pure (q y)] {True} ≤ ε) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ ε

A uniform bound on the event of every continuation bounds the event after a common draw. No losslessness of the draw is needed.

theorem le_prEvent_bind_of_forall_le {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (hmx : 𝒟[do let _ ← mx pure True] {True} = 1) (f : α → m β) (q : β → Prop) {ε : ENNReal} (h : ∀ (a : α), ε ≤ 𝒟[do let y ← f a pure (q y)] {True}) : ε ≤ 𝒟[do let y ← mx >>= f pure (q y)] {True}

A uniform lower bound on the event of every continuation bounds the event after a lossless common draw.

theorem mul_le_prEvent_bind_of_forall {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) {r r' : ENNReal} (h : r ≤ 𝒟[do let x ← mx pure (p x)] {True}) (h' : ∀ (x : α), p x → r' ≤ 𝒟[do let y ← f x pure (q y)] {True}) : r * r' ≤ 𝒟[do let y ← mx >>= f pure (q y)] {True}

Multiplying a lower bound for a prefix event by a uniform conditional lower bound gives a lower bound for the event after the bind.

theorem prEvent_bind_le_prEvent_add_mul_prEvent_not {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) {ε : ENNReal} (h : ∀ (a : α), ¬p a → 𝒟[do let y ← f a pure (q y)] {True} ≤ ε) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ 𝒟[do let a ← mx pure (p a)] {True} + ε * 𝒟[do let a ← mx pure ¬p a] {True}

Conditioning on a predicate of the common draw: the continuation event is bounded by the predicate's probability plus the conditional bound weighted by the predicate's complement. The weighting is the honest subprobability form; for a lossless draw the complement's probability is 1 - Pr{let a ← mx}[p a] by prEvent_add_prEvent_not.

theorem prEvent_bind_le_prEvent_of_forall_eq_zero {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) (h : ∀ (a : α), ¬p a → 𝒟[do let y ← f a pure (q y)] {True} = 0) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ 𝒟[do let a ← mx pure (p a)] {True}

A continuation event vanishing outside a predicate of the common draw is bounded by the predicate's probability.

theorem prEvent_bind_le_prEvent_add {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) {ε : ENNReal} (h : ∀ (a : α), ¬p a → 𝒟[do let y ← f a pure (q y)] {True} ≤ ε) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ 𝒟[do let a ← mx pure (p a)] {True} + ε

A continuation event bounded by ε outside a predicate of the common draw is bounded by the predicate's probability plus ε.

Reachable continuations through core attachment

Bounds that only hold on structurally reachable outputs of the common draw factor the bind through MonadAttach.attach, whose outputs carry their reachability proof.

theorem bind_eq_attach_bind {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α β : Type} (mx : m α) (f : α → m β) : mx >>= f = do let a ← MonadAttach.attach mx f ↑a

A bind factors through the attachment of its possible outputs.

theorem prEvent_true_attach {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α : Type} (mx : m α) : 𝒟[do let _ ← MonadAttach.attach mx pure True] {True} = 𝒟[do let _ ← mx pure True] {True}

The trivially true event is unchanged by attachment.

theorem prEvent_mono_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α : Type} (mx : m α) (p q : α → Prop) (h : ∀ a ∈ support mx, p a → q a) : 𝒟[do let a ← mx pure (p a)] {True} ≤ 𝒟[do let a ← mx pure (q a)] {True}

Implication between events only on the structurally reachable outputs bounds their probabilities.

theorem prEvent_bind_le_of_forall_le_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α β : Type} (mx : m α) (f : α → m β) (q : β → Prop) {ε : ENNReal} (h : ∀ a ∈ support mx, 𝒟[do let y ← f a pure (q y)] {True} ≤ ε) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ ε

A bound on the event of every reachable continuation bounds the event after the draw.

theorem le_prEvent_bind_of_forall_le_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α β : Type} (mx : m α) (hmx : 𝒟[do let _ ← mx pure True] {True} = 1) (f : α → m β) (q : β → Prop) {ε : ENNReal} (h : ∀ a ∈ support mx, ε ≤ 𝒟[do let y ← f a pure (q y)] {True}) : ε ≤ 𝒟[do let y ← mx >>= f pure (q y)] {True}

A lower bound on the event of every reachable continuation bounds the event after a lossless draw.

theorem prEvent_bind_le_prEvent_add_mul_prEvent_not_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) {ε : ENNReal} (h : ∀ a ∈ support mx, ¬p a → 𝒟[do let y ← f a pure (q y)] {True} ≤ ε) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ 𝒟[do let a ← mx pure (p a)] {True} + ε * 𝒟[do let a ← mx pure ¬p a] {True}

Conditioning on a predicate of the reachable common draw.

theorem prEvent_bind_le_prEvent_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) (h : ∀ a ∈ support mx, ¬p a → 𝒟[do let y ← f a pure (q y)] {True} = 0) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ 𝒟[do let a ← mx pure (p a)] {True}

A continuation event vanishing outside a predicate of the reachable draw is bounded by the predicate's probability.

theorem prEvent_bind_le_prEvent_add_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α β : Type} (mx : m α) (f : α → m β) (p : α → Prop) (q : β → Prop) {ε : ENNReal} (h : ∀ a ∈ support mx, ¬p a → 𝒟[do let y ← f a pure (q y)] {True} ≤ ε) : 𝒟[do let y ← mx >>= f pure (q y)] {True} ≤ 𝒟[do let a ← mx pure (p a)] {True} + ε

A continuation event bounded outside a predicate of the reachable draw.