Discrete subprobability monad

Discreteness invariant

A measure on the discrete (⊤) σ-algebra is discrete when it is the sum of its point masses, μ A = ∑_{x ∈ A} μ {x}. This is the invariant our semantics always satisfies (every measure is built from pure/bind/uniform/⊥), and it is exactly what lets the framework reconstruct a measure from its singletons and swap integration order without any countability assumption on the type — replacing the [Countable a] side-conditions (the goal of subtask 4).

def GaudisCrypt.discreteMeasure {a : Type u} (mu : MeasureTheory.Measure a) : Prop

A measure on the discrete σ-algebra is discrete (purely atomic) when μ A = ∑_{x∈A} μ{x}.

Equations

• GaudisCrypt.discreteMeasure mu = ∀ (A : Set a), mu A = ∑' (x : ↑A), mu {↑x}

theorem GaudisCrypt.discreteMeasure_zero {a : Type u} : discreteMeasure 0

theorem GaudisCrypt.discreteMeasure_dirac {a : Type u} (x : a) : discreteMeasure (MeasureTheory.Measure.dirac x)

theorem GaudisCrypt.discreteMeasure.eq_sum {a : Type u} {mu : MeasureTheory.Measure a} (hmu : discreteMeasure mu) : mu = MeasureTheory.Measure.sum fun (x : a) => mu {x} • MeasureTheory.Measure.dirac x

Structural form: a discrete measure is the Measure.sum of its weighted point masses.

theorem GaudisCrypt.discreteMeasure.ext {a : Type u} {mu nu : MeasureTheory.Measure a} (hmu : discreteMeasure mu) (hnu : discreteMeasure nu) (h : ∀ (z : a), mu {z} = nu {z}) : mu = nu

Singleton extensionality: two discrete measures agreeing on all singletons are equal (countability-free — the replacement for Measure.ext_of_singleton, which needs [Countable]).

theorem GaudisCrypt.lintegral_eq_tsum_smul {a : Type u} {mu : MeasureTheory.Measure a} (hmu : discreteMeasure mu) (g : a → ENNReal) : ∫⁻ (x : a), g x ∂mu = ∑' (x : a), mu {x} * g x

Integration against a discrete measure is the weighted sum of point evaluations.

theorem GaudisCrypt.lintegral_lintegral_swap_discrete {α s : Type u} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure s} (hμ : discreteMeasure μ) (hν : discreteMeasure ν) (g : α → s → ENNReal) : ∫⁻ (st' : s), ∫⁻ (a : α), g a st' ∂μ ∂ν = ∫⁻ (a : α), ∫⁻ (st' : s), g a st' ∂ν ∂μ

Fubini for discrete measures — integration order swaps with no σ-finiteness/countability side-condition, via ENNReal.tsum_comm.

theorem GaudisCrypt.discreteMeasure_bind {a b : Type u} {mu : MeasureTheory.Measure a} (hmu : discreteMeasure mu) {k : a → MeasureTheory.Measure b} (hk : ∀ (x : a), discreteMeasure (k x)) : discreteMeasure (mu.bind k)

Bind preserves discreteness (the keystone — countability-free, via ENNReal.tsum_comm).

theorem GaudisCrypt.discreteMeasure_pmf {a : Type u} (p : PMF a) : discreteMeasure p.toMeasure

theorem GaudisCrypt.discreteMeasure_iSup {a : Type u} (mu : ℕ → MeasureTheory.Measure a) (hmono : Monotone mu) (hd : ∀ (n : ℕ), discreteMeasure (mu n)) : discreteMeasure (⨆ (n : ℕ), mu n)

A monotone supremum of discrete measures is discrete (for the ωSup of the OCPO).

theorem GaudisCrypt.discreteMeasure_smul {a : Type u} (c : ENNReal) {mu : MeasureTheory.Measure a} (hmu : discreteMeasure mu) : discreteMeasure (c • mu)

Scaling preserves discreteness.

theorem GaudisCrypt.discreteMeasure_measureSum {a : Type u} {ι : Type v} (ν : ι → MeasureTheory.Measure a) (hν : ∀ (i : ι), discreteMeasure (ν i)) : discreteMeasure (MeasureTheory.Measure.sum ν)

A Measure.sum of discrete measures is discrete (countability-free, via ENNReal.tsum_comm).

theorem GaudisCrypt.discreteMeasure_sum_dirac {a : Type u} (w : a → ENNReal) : discreteMeasure (MeasureTheory.Measure.sum fun (t : a) => w t • MeasureTheory.Measure.dirac t)

The canonical discrete measure ∑ₜ w t • δₜ is discrete.

theorem GaudisCrypt.discreteMeasure_measure_iUnion {a : Type u} {ι : Type v} {mu : MeasureTheory.Measure a} (hmu : discreteMeasure mu) (B : ι → Set a) (hd : Pairwise (Function.onFun Disjoint B)) : mu (⋃ (i : ι), B i) = ∑' (i : ι), mu (B i)

Countable additivity over an arbitrary disjoint family for a discrete measure — the countability-free replacement for measure_iUnion (the index ι may be uncountable; the measure's countable support makes the sum well-defined). Proved by reindexing the singleton-sum across the disjoint union (ENNReal.tsum_sigma' + Set.unionEqSigmaOfDisjoint).

The sub-probability monad

def GaudisCrypt.SubProbability (a : Type u) : Type u

Equations

• GaudisCrypt.SubProbability a = { mu : MeasureTheory.Measure a // mu ⊤ ≤ 1 ∧ GaudisCrypt.discreteMeasure mu }

@[implicit_reducible]

noncomputable instance GaudisCrypt.instMonadSubProbability : Monad SubProbability

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaudisCrypt.toSubProbability {α : Type u_1} (p : PMF α) : SubProbability α

Equations

• GaudisCrypt.toSubProbability p = ⟨p.toMeasure, ⋯⟩

noncomputable def GaudisCrypt.SubProbability.uniform {α : Type u_1} [h : Fintype α] : [Nonempty α] → SubProbability α

Equations

• GaudisCrypt.SubProbability.uniform = GaudisCrypt.toSubProbability (PMF.uniformOfFintype α)

def GaudisCrypt.SubProbability.ofEvent {a : Type u_1} (μ : SubProbability a) (e : Set a) : NNReal

Equations

• μ.ofEvent e = (↑μ e).toNNReal

def GaudisCrypt.SubProbability.mass {a : Type u_1} (μ : SubProbability a) : NNReal

The total weight (mass) of a sub-probability: the measure of the whole space. 1 for a genuine probability, less when the computation can fail. The observable behind Footprint.indistinguishable. TODO: remove that and use : ofEvent ⊤ instead

Equations

• μ.mass = μ.ofEvent Set.univ

theorem GaudisCrypt.SubProbability.mass_bind_dirac {α β : Type} (μ : SubProbability α) (f : α → β) : (do let x ← μ pure (f x)).mass = μ.mass

Post-composing with a deterministic (Dirac) kernel preserves the total weight.

@[implicit_reducible]

instance GaudisCrypt.instCoeFunSubProbabilityForallNNReal {a : Type u_1} : CoeFun (SubProbability a) fun (x : SubProbability a) => a → NNReal

Equations

• GaudisCrypt.instCoeFunSubProbabilityForallNNReal = { coe := fun (μ : GaudisCrypt.SubProbability a) (x : a) => μ.ofEvent {x} }

@[implicit_reducible]

instance GaudisCrypt.instFunLikeSubProbabilityNNReal {a : Type u_1} : FunLike (SubProbability a) a NNReal

Equations

• GaudisCrypt.instFunLikeSubProbabilityNNReal = { coe := fun (μ : GaudisCrypt.SubProbability a) (x : a) => μ.ofEvent {x}, coe_injective := ⋯ }

@[implicit_reducible]

instance GaudisCrypt.instPartialOrderSubProbability {a : Type u_1} : PartialOrder (SubProbability a)

Equations

• GaudisCrypt.instPartialOrderSubProbability = { le := fun (p q : GaudisCrypt.SubProbability a) => ↑p ≤ ↑q, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance GaudisCrypt.instOrderBotSubProbability {a : Type u_1} : OrderBot (SubProbability a)

Equations

• GaudisCrypt.instOrderBotSubProbability = { bot := ⟨0, ⋯⟩, bot_le := ⋯ }

@[implicit_reducible]

noncomputable instance GaudisCrypt.instOmegaCompletePartialOrderSubProbability {a : Type u_1} : OmegaCompletePartialOrder (SubProbability a)

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.Measure.bind_mono {a : Type u_1} {b : Type u_2} {i : Type u_3} [MeasurableSpace a] [MeasurableSpace b] [Preorder i] (f : i → MeasureTheory.Measure a) (g : i → a → MeasureTheory.Measure b) (hf : Monotone f) (hg : Monotone g) (hgm : ∀ (x : i), Measurable (g x)) : Monotone fun (x : i) => (f x).bind (g x)

theorem GaudisCrypt.Measure.bind_ωScottContinuous {b : Type u_1} {c : Type u_2} {a : Type u_3} [MeasurableSpace b] [MeasurableSpace c] [OmegaCompletePartialOrder a] (f : a → MeasureTheory.Measure b) (g : a → b → MeasureTheory.Measure c) (hgm : ∀ (x : a), Measurable (g x)) (hg : OmegaCompletePartialOrder.ωScottContinuous g) (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : a) => (f x).bind (g x)

theorem GaudisCrypt.SubProbability.bind_ωScottContinuous {a : Type u_1} {b c : Type u_2} [OmegaCompletePartialOrder a] (f : a → SubProbability b) (g : a → b → SubProbability c) (hg : OmegaCompletePartialOrder.ωScottContinuous g) (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : a) => f x >>= g x

theorem GaudisCrypt.SubProbability.bind_mono {i : Type u_1} {a b : Type u_2} [Preorder i] (f : i → SubProbability a) (g : i → a → SubProbability b) (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : i) => f x >>= g x

theorem GaudisCrypt.SubProbability.pure_bind {α β : Type} (x : α) (f : α → SubProbability β) : pure x >>= f = f x

theorem GaudisCrypt.SubProbability.bind_assoc {α β γ : Type} (m : SubProbability α) (f : α → SubProbability β) (g : β → SubProbability γ) : m >>= f >>= g = m >>= fun (x : α) => f x >>= g

theorem GaudisCrypt.SubProbability.bind_pure {α : Type} (m : SubProbability α) : m >>= pure = m

@[simp]

theorem GaudisCrypt.SubProbability.mass_pure {α : Type} (x : α) : (pure x).mass = 1

@[simp]

theorem GaudisCrypt.SubProbability.mass_bot {α : Type} : ⊥.mass = 0

theorem GaudisCrypt.SubProbability.bind_const_pure {α β : Type} (ν : SubProbability α) (hν : ↑ν Set.univ = 1) (b : β) : (do let _ ← ν pure b) = pure b

Binding a probability (total mass 1) into a constant pure collapses to that pure: a lossless computation whose result is discarded is invisible.

theorem GaudisCrypt.SubProbability.bot_bind {α β : Type} (f : α → SubProbability β) : ⊥ >>= f = ⊥

theorem GaudisCrypt.SubProbability.bind_bot {α β : Type} (m : SubProbability α) : (do let _ ← m ⊥) = ⊥

@[implicit_reducible]

noncomputable instance GaudisCrypt.instMonoidForallSubProbability {m : Type u_1} : Monoid (m → SubProbability m)

Kleisli composition for SubProbability: f * g applies g first, then f on the result (so f * g = f ∘ₖ g), with pure as the identity. This is the monoid of sub-probability kernels m → SubProbability m, the probabilistic analogue of Function.End.

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.SubProbability.pure_injective {a : Type} : Function.Injective pure

pure is injective on SubProbability (it is the Dirac embedding): pure x = pure y → x = y. Lets us extract a plain pointwise state equation from a Dirac-kernel commutation identity.

theorem GaudisCrypt.SubProbability.double_commutant_mono {m : Type u_1} {A B : Set (m → SubProbability m)} (h : A ⊆ B) : A.centralizer.centralizer ⊆ B.centralizer.centralizer

Bicommutant closure is monotone.