Measure-valued evaluation and its composition laws

EvalDistSemantics denotes successful outputs by subprobability measures. LawfulPureEvalDistSemantics supplies the Dirac equation independently of bind, while LawfulEvalDistSemantics adds the measurable-bind equation. Measurable spaces and continuations are explicit; discrete source spaces discharge continuation measurability without constraining the result space.

class EvalDistSemantics (m : Type u → Type v) : Type (max (u + 1) v)

A measure-valued subprobability semantics for a type constructor.

• denote {α : Type u} [MeasurableSpace α] : m α → MeasureTheory.Measure α

  Interpret a computation as its measure of successful outputs.

• apply_univ_le_one {α : Type u} [MeasurableSpace α] (mx : m α) : (denote mx) Set.univ ≤ 1

  Successful output mass is at most one.

@[reducible, inline]

noncomputable def evalDist {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) : MeasureTheory.Measure α

The measure of successful outputs produced by mx.

def «term𝒟[_]» : Lean.ParserDescr

Evaluation-measure notation.

theorem evalDist_ite {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (p : Prop) [Decidable p] (mx my : m α) : 𝒟[if p then mx else my] = if p then 𝒟[mx] else 𝒟[my]

Denotation commutes with conditional choice of a computation.

theorem evalDist_dite {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (p : Prop) [Decidable p] (mx : p → m α) (my : ¬p → m α) : 𝒟[if h : p then mx h else my h] = if h : p then 𝒟[mx h] else 𝒟[my h]

Denotation commutes with dependent conditional choice of a computation.

@[simp]

theorem evalDist_ite_apply {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (p : Prop) [Decidable p] (mx my : m α) (s : Set α) : 𝒟[if p then mx else my] s = if p then 𝒟[mx] s else 𝒟[my] s

The mass of an event commutes with conditional choice of a computation.

@[simp]

theorem evalDist_dite_apply {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (p : Prop) [Decidable p] (mx : p → m α) (my : ¬p → m α) (s : Set α) : 𝒟[if h : p then mx h else my h] s = if h : p then 𝒟[mx h] s else 𝒟[my h] s

Event mass commutes with dependent conditional choice of a computation.

theorem evalDist_apply_univ_le_one {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) : 𝒟[mx] Set.univ ≤ 1

instance evalDist.instIsSubprobabilityMeasure {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) : MeasureTheory.IsSubprobabilityMeasure 𝒟[mx]

Every computation denotation is a subprobability measure.

@[simp]

theorem evalDist_apply_le_one {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) (s : Set α) : 𝒟[mx] s ≤ 1

No event of a computation has mass above one.

class LawfulPureEvalDistSemantics (m : Type u → Type v) [Monad m] [EvalDistSemantics m] : Prop

A measure-valued semantics sends pure to a Dirac measure. This law is separate from the bind law because a semantics can preserve pure even when continuous effects prevent a global measurability proof for arbitrary bind continuations.

• denote_pure {α : Type u} [MeasurableSpace α] (x : α) : 𝒟[pure x] = MeasureTheory.Measure.dirac x

  pure denotes a Dirac measure.

class LawfulEvalDistSemantics (m : Type u → Type v) [Monad m] [EvalDistSemantics m] extends LawfulPureEvalDistSemantics m : Prop

A measure-valued semantics also respects measurable bind in the Giry monad.

• denote_pure {α : Type u} [MeasurableSpace α] (x : α) : 𝒟[pure x] = MeasureTheory.Measure.dirac x
• denote_bind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (x : α) => 𝒟[f x]) : 𝒟[mx >>= f] = 𝒟[mx].bind fun (x : α) => 𝒟[f x]

  Monadic bind denotes Giry bind whenever its measure-valued continuation is measurable.

@[simp]

theorem evalDist_pure {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (x : α) : 𝒟[pure x] = MeasureTheory.Measure.dirac x

instance evalDist.instIsProbabilityMeasurePure {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (x : α) : MeasureTheory.IsProbabilityMeasure 𝒟[pure x]

theorem evalDist_bind {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (x : α) => 𝒟[f x]) : 𝒟[mx >>= f] = 𝒟[mx].bind fun (x : α) => 𝒟[f x]

theorem evalDist_bind_of_discrete {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) : 𝒟[mx >>= f] = 𝒟[mx].bind fun (x : α) => 𝒟[f x]

On a discrete source type, every measure-valued continuation is measurable.

theorem evalDist_bind_congr_ae {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f g : α → m β) (hf : Measurable fun (x : α) => 𝒟[f x]) (hg : Measurable fun (x : α) => 𝒟[g x]) (h : (fun (x : α) => 𝒟[f x]) =ᵐ[𝒟[mx]] fun (x : α) => 𝒟[g x]) : 𝒟[mx >>= f] = 𝒟[mx >>= g]

Almost-everywhere equal measurable continuation measures give equal composed measures.

theorem evalDist_bind_congr {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace β] (mx : m α) (f g : α → m β) (h : ∀ (x : α), 𝒟[f x] = 𝒟[g x]) : 𝒟[mx >>= f] = 𝒟[mx >>= g]

Pointwise equality of continuation measures gives equality after a common bind. No measurable structure is required on the unobserved intermediate type: the common continuation measure supplies its observation's pullback measurable space.

theorem evalDist_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) {f : α → β} (hf : Measurable f) : 𝒟[f <$> mx] = MeasureTheory.Measure.map f 𝒟[mx]

Functor.map along a measurable function denotes the pushforward measure.

theorem evalDist_map_of_discrete {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → β) : 𝒟[f <$> mx] = MeasureTheory.Measure.map f 𝒟[mx]

On a discrete source type, every Functor.map denotes a pushforward.

theorem evalDist_pair {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) : 𝒟[do let x ← mx let y ← my pure (x, y)] = 𝒟[mx].prod 𝒟[my]

Independent sequential draws denote Mathlib's product measure.

@[simp]

theorem evalDist_bind_const {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) : 𝒟[do let _ ← mx my] = 𝒟[mx] Set.univ • 𝒟[my]

A constant continuation scales the continuation's measure by the success mass (Measure.bind_const); the measure form of probOutput_bind_const.

@[simp]

theorem evalDist_map_const {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (c : β) : 𝒟[(fun (x : α) => c) <$> mx] = 𝒟[mx] Set.univ • MeasureTheory.Measure.dirac c

A constant map denotes the success mass at a point (Measure.map_const); the measure form of probOutput_map_const.

theorem lintegral_evalDist_bind_of_aemeasurable {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (x : α) => 𝒟[f x]) {g : β → ENNReal} (hg : AEMeasurable g 𝒟[mx >>= f]) : ∫⁻ (y : β), g y ∂𝒟[mx >>= f] = ∫⁻ (x : α), ∫⁻ (y : β), g y ∂𝒟[f x] ∂𝒟[mx]

An AE-measurable valuation of composed outputs satisfies the integral tower law.

theorem lintegral_evalDist_bind {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (x : α) => 𝒟[f x]) {g : β → ENNReal} (hg : Measurable g) : ∫⁻ (y : β), g y ∂𝒟[mx >>= f] = ∫⁻ (x : α), ∫⁻ (y : β), g y ∂𝒟[f x] ∂𝒟[mx]

Integrating a bind first integrates each measurable continuation, then its common draw.

theorem lintegral_evalDist_bind_of_discrete {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) {g : β → ENNReal} (hg : Measurable g) : ∫⁻ (y : β), g y ∂𝒟[mx >>= f] = ∫⁻ (x : α), ∫⁻ (y : β), g y ∂𝒟[f x] ∂𝒟[mx]

For a discrete common draw, the tower law needs no continuation measurability proof.

theorem lintegral_evalDist_map_of_aemeasurable {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) {f : α → β} (hf : Measurable f) {g : β → ENNReal} (hg : AEMeasurable g 𝒟[f <$> mx]) : ∫⁻ (y : β), g y ∂𝒟[f <$> mx] = ∫⁻ (x : α), g (f x) ∂𝒟[mx]

An AE-measurable valuation of a measurable output map integrates the composed functional.

theorem lintegral_evalDist_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) {f : α → β} (hf : Measurable f) {g : β → ENNReal} (hg : Measurable g) : ∫⁻ (y : β), g y ∂𝒟[f <$> mx] = ∫⁻ (x : α), g (f x) ∂𝒟[mx]

Integrating a measurable output map integrates the composed functional.

@[simp]

theorem lintegral_evalDist_map_of_discrete {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] (mx : m α) (f : α → β) (g : β → ENNReal) : ∫⁻ (y : β), g y ∂𝒟[f <$> mx] = ∫⁻ (x : α), g (f x) ∂𝒟[mx]

On discrete source and target spaces, output-map integration needs no measurability proofs.

@[simp]

theorem lintegral_evalDist_map_add_nat {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (f : α → ℕ) (c : ℕ) : ∫⁻ (n : ℕ), ↑n ∂𝒟[(fun (x : α) => f x + c) <$> mx] = ∫⁻ (n : ℕ), ↑n ∂𝒟[f <$> mx] + ↑c * 𝒟[f <$> mx] Set.univ

Adding to a natural-valued observation adds the constant scaled by the successful output mass. The observed computation's intermediate result needs no measurable-space instance.

theorem lintegral_evalDist_map_const_add_nat {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (f : α → ℕ) (c : ℕ) : ∫⁻ (n : ℕ), ↑n ∂𝒟[c.add <$> f <$> mx] = ∫⁻ (n : ℕ), ↑n ∂𝒟[f <$> mx] + ↑c * 𝒟[f <$> mx] Set.univ

Adding a fixed natural to an observed count scales that increment by successful mass. The curried addition form supplies a binder-free pattern for grind.

theorem evalDist_bind_apply_univ {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (x : α) => 𝒟[f x]) : 𝒟[mx >>= f] Set.univ = ∫⁻ (x : α), 𝒟[f x] Set.univ ∂𝒟[mx]

The success mass of a bind is the integral of its continuation's success mass.

theorem evalDist_map_apply_univ {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) {f : α → β} (hf : Measurable f) : 𝒟[f <$> mx] Set.univ = 𝒟[mx] Set.univ

A measurable map preserves the successful-output mass.

theorem evalDist_pure_apply_le_of_imp {m : Type → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] (a b : Bool) (h : a = true → b = true) : 𝒟[pure a] {true} ≤ 𝒟[pure b] {true}

Implication between Boolean results bounds their pure successful masses.

theorem evalDist_pure_apply_le_add_of_imp {m : Type → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] (a b c : Bool) (h : a = true → b = true ∨ c = true) : 𝒟[pure a] {true} ≤ 𝒟[pure b] {true} + 𝒟[pure c] {true}

A pure Boolean result covered by either of two results has mass bounded by their sum.