Measure events for computation notation

Pr{...}[...] interprets an ordinary Lean do computation as the successful-output measure of its Boolean or propositional result. These equations identify that measure with an event in the underlying computation when the event is measurable.

def prEvent : Lean.ParserDescr

Probability of a successful event after an ordinary Lean do sequence. The event is interpreted by the primary measure semantics.

def prEventFormatter : Lean.PrettyPrinter.Formatter

Format an event sequence directly after its opening delimiter, keeping the ordinary Lean formatter for subsequent statements and explicitly braced sequences. Explicit line breaks after the opening delimiter are preserved.

theorem prEvent_eq_evalDist_map {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[p <$> mx] {True}

An event is the true mass of its propositional selector.

theorem prEvent_eq_evalDist {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] (mx : m α) (p : α → Prop) (hp : Measurable p) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[mx] {x : α | p x}

A measurable predicate returned by a computation has the probability of its event.

theorem prEvent_eq_evalDist_of_discrete {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] [DiscreteMeasurableSpace α] (mx : m α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[mx] {x : α | p x}

On a discrete output space every predicate is a measurable event.

theorem prEvent_eq_evalDist_singleton {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] [MeasurableSingletonClass α] (mx : m α) (a : α) : 𝒟[do let x ← mx pure (x = a)] {True} = 𝒟[mx] {a}

Equality to one output has its singleton mass whenever singletons are measurable.

theorem prEvent_eq_evalDist_decide {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) [DecidablePred p] : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[do let x ← mx pure (decide (p x))] {true}

A final decidable event has the same success mass whether it is returned as a proposition or decided to a Boolean; no measurable structure on intermediate values is needed.

theorem prEvent_congr {m : Type → Type v} [Monad m] [EvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) (h : ∀ (x : α), p x ↔ q x) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[do let x ← mx pure (q x)] {True}

Pointwise equivalent predicates have the same probability after a common computation.

theorem prEvent_congr_ae {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] (mx : m α) (p q : α → Prop) (hp : Measurable p) (hq : Measurable q) (h : ∀ᵐ (x : α) ∂𝒟[mx], p x ↔ q x) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[do let x ← mx pure (q x)] {True}

Measurable predicates agreeing almost everywhere have equal event probabilities.

theorem prEvent_eq_zero_of_forall_not {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) (h : ∀ (x : α), ¬p x) : 𝒟[do let x ← mx pure (p x)] {True} = 0

An event that never occurs has probability zero.

theorem prEvent_mono_ae {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] (mx : m α) (p q : α → Prop) (hp : Measurable p) (hq : Measurable q) (hpq : ∀ᵐ (x : α) ∂𝒟[mx], p x → q x) : 𝒟[do let x ← mx pure (p x)] {True} ≤ 𝒟[do let x ← mx pure (q x)] {True}

Almost-everywhere implication bounds probabilities of measurable events.

theorem prEvent_mono_of_discrete {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] [DiscreteMeasurableSpace α] (mx : m α) (p q : α → Prop) (hpq : ∀ (x : α), p x → q x) : 𝒟[do let x ← mx pure (p x)] {True} ≤ 𝒟[do let x ← mx pure (q x)] {True}

Implication between events bounds their probabilities on a discrete output space.

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

Implication between final events bounds their probabilities without a measurable-space argument on the intermediate values.

theorem prEvent_bind_eq_lintegral {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} [MeasurableSpace α] (mx : m α) (f : α → m β) (p : β → Prop) (hf : Measurable fun (x : α) => 𝒟[do let y ← f x pure (p y)]) : 𝒟[do let y ← mx >>= f pure (p y)] {True} = ∫⁻ (x : α), 𝒟[do let y ← f x pure (p y)] {True} ∂𝒟[mx]

An observed bind integrates the event probability of each measurable continuation. Only the common draw needs a selected measurable space; the continuation is observed in Prop.

theorem prEvent_bind_eq_lintegral_of_discrete {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} [MeasurableSpace α] [DiscreteMeasurableSpace α] (mx : m α) (f : α → m β) (p : β → Prop) : 𝒟[do let y ← mx >>= f pure (p y)] {True} = ∫⁻ (x : α), 𝒟[do let y ← f x pure (p y)] {True} ∂𝒟[mx]

A discrete common draw discharges the observed continuation's measurability.

theorem prEvent_bind_congr_ae {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type} [MeasurableSpace α] (mx : m α) (f : α → m β) (g : α → m γ) (p : β → Prop) (q : γ → Prop) (hf : Measurable fun (x : α) => 𝒟[do let y ← f x pure (p y)]) (hg : Measurable fun (x : α) => 𝒟[do let z ← g x pure (q z)]) (h : ∀ᵐ (x : α) ∂𝒟[mx], 𝒟[do let y ← f x pure (p y)] {True} = 𝒟[do let z ← g x pure (q z)] {True}) : 𝒟[do let y ← mx >>= f pure (p y)] {True} = 𝒟[do let z ← mx >>= g pure (q z)] {True}

AE equality of measurable observed continuation probabilities gives equality after a draw.

theorem prEvent_bind_congr {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type} (mx : m α) (f : α → m β) (g : α → m γ) (p : β → Prop) (q : γ → Prop) (h : ∀ (x : α), 𝒟[do let y ← f x pure (p y)] {True} = 𝒟[do let z ← g x pure (q z)] {True}) : 𝒟[do let y ← mx >>= f pure (p y)] {True} = 𝒟[do let z ← mx >>= g pure (q z)] {True}

Pointwise equality of observed continuation probabilities gives equality after a common draw. Neither the draw nor the continuation outputs need a measurable-space argument.

theorem prEvent_map {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] {α β : Type} (mx : m α) (f : α → β) (p : β → Prop) : 𝒟[do let y ← f <$> mx pure (p y)] {True} = 𝒟[do let x ← mx pure (p (f x))] {True}

An output map composes the final event with that map.

@[simp]

theorem prEvent_bind_bind_and {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (my : m β) (p : α → Prop) (q : β → Prop) : 𝒟[do let x ← mx let y ← my pure (p x ∧ q y)] {True} = 𝒟[do let x ← mx pure (p x)] {True} * 𝒟[do let y ← my pure (q y)] {True}

Events of independent draws have the product of their probabilities.

theorem prEvent_le_one {m : Type → Type v} [Monad m] [EvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} ≤ 1

Every event probability is at most one.

theorem prEvent_true_eq_evalDist_apply_univ {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) : 𝒟[do let _ ← mx pure True] {True} = 𝒟[mx] Set.univ

The trivially true event is the successful mass of the computation, observed in the discrete structure on its outputs.

theorem prEvent_congr_of_evalDist_eq {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx my : m α) (h : 𝒟[mx] = 𝒟[my]) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[do let y ← my pure (p y)] {True}

Computations with the same output measure in the discrete structure have the same events.

theorem prEvent_const_of_lossless {m : Type → Type v} [Monad m] [EvalDistSemantics m] {α : Type} (mx : m α) (hmx : 𝒟[do let _ ← mx pure True] {True} = 1) {c : Prop} (hc : c) : 𝒟[do let _ ← mx pure c] {True} = 1

A true constant event after a lossless draw has probability one.

theorem prEvent_const_of_not {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) {c : Prop} (hc : ¬c) : 𝒟[do let _ ← mx pure c] {True} = 0

A false constant event has probability zero.