Probabilistic powerdomain (sections 4.1–4.4)

This file follows Sections 4.1–4.4 of [VKS19]. It records the basic structures (randomizations, expectation operators, sampling, scoring, closures under ω-sups).

@[reducible, inline]

abbrev OmegaQuasiBorelSpace.Randomization (X : Type u_3) [OmegaQuasiBorelSpace X] : Type u_3

Randomizations of X are partial maps from the randomness source

Equations

• OmegaQuasiBorelSpace.Randomization X = (FlatReal →ω𝒒 Option X)

def OmegaQuasiBorelSpace.Randomization.dom {X : Type u_1} [OmegaQuasiBorelSpace X] (α : Randomization X) : Set FlatReal

Domain of a randomization.

Equations

• α.dom = {r : FlatReal | α r ≠ none}

noncomputable def OmegaQuasiBorelSpace.expectation {X : Type u_1} [OmegaQuasiBorelSpace X] : Randomization X →ω𝒒 Cont ENNReal X

The expectation morphism expectation : Randomization → JX.

Equations

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

@[simp]

theorem OmegaQuasiBorelSpace.expectation_coe_apply_coe {X : Type u_1} [OmegaQuasiBorelSpace X] (α : Randomization X) (w : X →ω𝒒 ENNReal) : (expectation α).apply w = ∫⁻ (r : FlatReal), (α r).elim 0 ⇑w

noncomputable def OmegaQuasiBorelSpace.Randomization.pure {X : Type u_1} [OmegaQuasiBorelSpace X] (x : X) : Randomization X

Monad unit on randomizations (Dirac)

Equations

• OmegaQuasiBorelSpace.Randomization.pure x = { toFun := fun (r : FlatReal) => if r.val ∈ Set.Icc 0 1 then some x else none, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelSpace.Randomization.pure_coe {X : Type u_1} [OmegaQuasiBorelSpace X] (x : X) (r : FlatReal) : (pure x) r = if r.val ∈ Set.Icc 0 1 then some x else none

class OmegaQuasiBorelSpace.RandomSplit : Type

A measurable splitting of randomness as in the transfer principle

• φ : FlatReal → FlatReal × FlatReal

  The splitting function

• measurable_φ : Measurable φ

  The splitting function is measurable

• preserves_volume : MeasureTheory.Measure.map φ MeasureTheory.volume = MeasureTheory.volume.prod MeasureTheory.volume

  Pushing forward Lebesgue along the split yields the product measure

def OmegaQuasiBorelSpace.Randomization.bind {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [RandomSplit] (α : Randomization X) (k : X →ω𝒒 Randomization Y) : Randomization Y

Monad bind on randomizations using the randomness splitting

Equations

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

@[simp]

theorem OmegaQuasiBorelSpace.Randomization.bind_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [RandomSplit] (α : Randomization X) (k : X →ω𝒒 Randomization Y) (r : FlatReal) : (α.bind k) r = (α (RandomSplit.φ r).1).bind fun (x : X) => (k x) (RandomSplit.φ r).2

theorem OmegaQuasiBorelSpace.expectation_preserves_return (X : Type u_3) [OmegaQuasiBorelSpace X] (x : X) : expectation (Randomization.pure x) = Cont.unit x

Expectation preserves the monad structure on randomizations

theorem OmegaQuasiBorelSpace.expectation_preserves_bind {Y : Type u_2} [OmegaQuasiBorelSpace Y] (X : Type u_3) [OmegaQuasiBorelSpace X] [RandomSplit] (α : Randomization X) (k : X →ω𝒒 Randomization Y) : expectation (α.bind k) = (Cont.bind (expectation.comp k)) (expectation α)

def OmegaQuasiBorelSpace.Randomizable (X : Type u_3) [OmegaQuasiBorelSpace X] (μ : Cont ENNReal X) : Prop

Predicate: expectation operator arising from a randomization

Equations

• OmegaQuasiBorelSpace.Randomizable X μ = ∃ (α : OmegaQuasiBorelSpace.Randomization X), μ = OmegaQuasiBorelSpace.expectation α

def OmegaQuasiBorelSpace.RandomizableExpectation (X : Type u_3) [OmegaQuasiBorelSpace X] : Type u_3

Randomizable expectation operators as a subtype

Equations

• OmegaQuasiBorelSpace.RandomizableExpectation X = { μ : OmegaQuasiBorelSpace.Cont ENNReal X // OmegaQuasiBorelSpace.Randomizable X μ }

@[reducible, inline]

abbrev OmegaQuasiBorelSpace.RandomElement (X : Type u_4) [OmegaQuasiBorelSpace X] : Type u_4

Random elements of X (using FlatReal as randomness)

Equations

• OmegaQuasiBorelSpace.RandomElement X = (FlatReal →ω𝒒 X)

@[reducible, inline]

abbrev OmegaQuasiBorelSpace.RandomizationRandomElement (X : Type u_4) [OmegaQuasiBorelSpace X] : Type u_4

Randomizations valued in randomizations.

Equations

• OmegaQuasiBorelSpace.RandomizationRandomElement X = OmegaQuasiBorelSpace.RandomElement (OmegaQuasiBorelSpace.Randomization X)

@[reducible, inline]

abbrev OmegaQuasiBorelSpace.RandomExpectation (X : Type u_4) [OmegaQuasiBorelSpace X] : Type u_4

Randomizable random operators (random elements of Cont ENNReal).

Equations

• OmegaQuasiBorelSpace.RandomExpectation X = OmegaQuasiBorelSpace.RandomElement (OmegaQuasiBorelSpace.Cont ENNReal X)

noncomputable def OmegaQuasiBorelSpace.expectationRandom (X : Type u_3) [OmegaQuasiBorelSpace X] (β : RandomizationRandomElement X) : RandomExpectation X

Extend expectation pointwise to random randomizations.

Equations

• OmegaQuasiBorelSpace.expectationRandom X β = { toFun := fun (r : FlatReal) => OmegaQuasiBorelSpace.expectation (β r), isHom' := ⋯, ωScottContinuous' := ⋯ }

inductive OmegaQuasiBorelSpace.InPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : Cont ENNReal X → Prop

Membership in the ω-sup-closure of randomizable operators

• randomizable {X : Type u_3} [OmegaQuasiBorelSpace X] (α : Randomization X) : InPowerdomain X (expectation α)

  Randomizable operators are in the closure

• sup {X : Type u_3} [OmegaQuasiBorelSpace X] {c : OmegaCompletePartialOrder.Chain (Cont ENNReal X)} : (∀ (n : ℕ), InPowerdomain X (c n)) → InPowerdomain X (OmegaCompletePartialOrder.ωSup c)

  The closure is closed under ω-sups

inductive OmegaQuasiBorelSpace.InRandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : RandomExpectation X → Prop

Membership in the ω-sup-closure of randomizable random operators

• randomizable {X : Type u_3} [OmegaQuasiBorelSpace X] (β : RandomizationRandomElement X) : InRandomPowerdomain X (expectationRandom X β)

  Randomizable random operators are in the closure

• sup {X : Type u_3} [OmegaQuasiBorelSpace X] {c : OmegaCompletePartialOrder.Chain (RandomExpectation X)} : (∀ (n : ℕ), InRandomPowerdomain X (c n)) → InRandomPowerdomain X (OmegaCompletePartialOrder.ωSup c)

  The closure is closed under ω-sups

@[reducible, inline]

abbrev OmegaQuasiBorelSpace.Powerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : Type u_3

Probabilistic powerdomain: smallest ω-subcpo of Cont ENNReal

Equations

• OmegaQuasiBorelSpace.Powerdomain X = { μ : OmegaQuasiBorelSpace.Cont ENNReal X // OmegaQuasiBorelSpace.InPowerdomain X μ }

@[reducible, inline]

abbrev OmegaQuasiBorelSpace.RandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : Type u_3

Random elements of the powerdomain

Equations

• OmegaQuasiBorelSpace.RandomPowerdomain X = { β : OmegaQuasiBorelSpace.RandomExpectation X // OmegaQuasiBorelSpace.InRandomPowerdomain X β }

noncomputable instance OmegaQuasiBorelSpace.instQuasiBorelSpacePowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : QuasiBorelSpace (Powerdomain X)

Equations

• OmegaQuasiBorelSpace.instQuasiBorelSpacePowerdomain X = id inferInstance

noncomputable instance OmegaQuasiBorelSpace.instQuasiBorelSpaceRandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : QuasiBorelSpace (RandomPowerdomain X)

Equations

• OmegaQuasiBorelSpace.instQuasiBorelSpaceRandomPowerdomain X = id inferInstance

noncomputable instance OmegaQuasiBorelSpace.instPartialOrderPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : PartialOrder (Powerdomain X)

Order structure on Powerdomain X inherited from the ambient Cont ENNReal

Equations

• OmegaQuasiBorelSpace.instPartialOrderPowerdomain X = id inferInstance

noncomputable instance OmegaQuasiBorelSpace.instPartialOrderRandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : PartialOrder (RandomPowerdomain X)

Order structure on RandomPowerdomain X inherited from RandomExpectation.

Equations

• OmegaQuasiBorelSpace.instPartialOrderRandomPowerdomain X = id inferInstance

def OmegaQuasiBorelSpace.Powerdomain.incl (X : Type u_3) [OmegaQuasiBorelSpace X] (t : Powerdomain X) : Cont ENNReal X

Inclusion of Powerdomain into Cont ENNReal

Equations

• OmegaQuasiBorelSpace.Powerdomain.incl X t = ↑t

def OmegaQuasiBorelSpace.RandomPowerdomain.incl (X : Type u_3) [OmegaQuasiBorelSpace X] (t : RandomPowerdomain X) : RandomExpectation X

Inclusion of RandomPowerdomain into RandomExpectation

Equations

• OmegaQuasiBorelSpace.RandomPowerdomain.incl X t = ↑t

noncomputable def OmegaQuasiBorelSpace.expectationPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] (α : Randomization X) : Powerdomain X

Expectation factors through Powerdomain.

Equations

• OmegaQuasiBorelSpace.expectationPowerdomain X α = ⟨OmegaQuasiBorelSpace.expectation α, ⋯⟩

noncomputable def OmegaQuasiBorelSpace.expectationRandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] (β : RandomizationRandomElement X) : RandomPowerdomain X

Pointwise extension of expectationPowerdomain to random randomizations.

Equations

• OmegaQuasiBorelSpace.expectationRandomPowerdomain X β = ⟨OmegaQuasiBorelSpace.expectationRandom X β, ⋯⟩

noncomputable instance OmegaQuasiBorelSpace.instOmegaCompletePartialOrderPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : OmegaCompletePartialOrder (Powerdomain X)

Powerdomain inherits an ωCPO structure from Cont ENNReal

Equations

• OmegaQuasiBorelSpace.instOmegaCompletePartialOrderPowerdomain X = OmegaCompletePartialOrder.subtype (fun (μ : OmegaQuasiBorelSpace.Cont ENNReal X) => OmegaQuasiBorelSpace.InPowerdomain X μ) ⋯

noncomputable instance OmegaQuasiBorelSpace.instPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : OmegaQuasiBorelSpace (Powerdomain X)

Powerdomain is an ωQBS as a full subobject of Cont ENNReal

Equations

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

@[simp]

theorem OmegaQuasiBorelSpace.Powerdomain.ωScottContinuous_val (X : Type u_3) [OmegaQuasiBorelSpace X] : OmegaCompletePartialOrder.ωScottContinuous fun (x : Powerdomain X) => ↑x

the val projection of TX is ω-scott continuous

theorem OmegaQuasiBorelSpace.Powerdomain.ωScottContinuous_val' (X : Type u_3) [OmegaQuasiBorelSpace X] {A : Type u_4} [OmegaCompletePartialOrder A] {f : A → Powerdomain X} (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : A) => ↑(f x)

composing with val preserves ω-scott continuity for Powerdomain

noncomputable instance OmegaQuasiBorelSpace.instOmegaCompletePartialOrderRandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : OmegaCompletePartialOrder (RandomPowerdomain X)

RandomPowerdomain inherits an ωCPO structure from RandomExpectation

Equations

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

noncomputable instance OmegaQuasiBorelSpace.instRandomPowerdomain (X : Type u_3) [OmegaQuasiBorelSpace X] : OmegaQuasiBorelSpace (RandomPowerdomain X)

RandomPowerdomain is an ωQBS as a full subobject of RandomExpectation

Equations

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

noncomputable def OmegaQuasiBorelSpace.Powerdomain.pure (X : Type u_3) [OmegaQuasiBorelSpace X] (x : X) : Powerdomain X

Monad unit on Powerdomain obtained by restriction

Equations

• OmegaQuasiBorelSpace.Powerdomain.pure X x = ⟨OmegaQuasiBorelSpace.Cont.unit x, ⋯⟩

noncomputable def OmegaQuasiBorelSpace.Powerdomain.bind {Y : Type u_2} [OmegaQuasiBorelSpace Y] (X : Type u_3) [OmegaQuasiBorelSpace X] (t : Powerdomain X) (k : X →ω𝒒 Powerdomain Y) : Powerdomain Y

Monad bind on Powerdomain, restricting the J bind

Equations

• OmegaQuasiBorelSpace.Powerdomain.bind X t k = ⟨(OmegaQuasiBorelSpace.Cont.bind { toFun := fun (x : X) => ↑(k x), isHom' := ⋯, ωScottContinuous' := ⋯ }) ↑t, ⋯⟩

theorem OmegaQuasiBorelSpace.expectation_factorizes_monad : True

(placeholder) The inclusion Powerdomain ↪ J is a monad morphism (See theorem 4.3 of [VKS19])

noncomputable def OmegaQuasiBorelSpace.Randomization.sample : Randomization FlatReal

sample : 1 → R R is the identity randomization on reals

Equations

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

noncomputable def OmegaQuasiBorelSpace.Randomization.score (r : FlatReal) : Randomization Unit

score : R → R⊥ truncates Lebesgue to an interval of length |r|

Equations

• OmegaQuasiBorelSpace.Randomization.score r = { toFun := fun (t : FlatReal) => if t.val ∈ Set.Icc 0 |r.val| then some () else none, isHom' := ⋯, ωScottContinuous' := ⋯ }

noncomputable def OmegaQuasiBorelSpace.Powerdomain.sample : Powerdomain FlatReal

Sampling lifted to the powerdomain

Equations

• OmegaQuasiBorelSpace.Powerdomain.sample = OmegaQuasiBorelSpace.expectationPowerdomain FlatReal OmegaQuasiBorelSpace.Randomization.sample

noncomputable def OmegaQuasiBorelSpace.Powerdomain.score (r : FlatReal) : Powerdomain Unit

Conditioning lifted to the powerdomain

Equations

• OmegaQuasiBorelSpace.Powerdomain.score r = OmegaQuasiBorelSpace.expectationPowerdomain Unit (OmegaQuasiBorelSpace.Randomization.score r)