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).

structure QuasiBorelSpaces.R : Type

Reals with the Lebesgue measure and a discrete ωCPO structure

• val : ℝ

  The underlying real number

instance QuasiBorelSpaces.instInhabitedR : Inhabited R

Equations

• QuasiBorelSpaces.instInhabitedR = { default := { val := 0 } }

instance QuasiBorelSpaces.instMeasurableSpaceR : MeasurableSpace R

Equations

• QuasiBorelSpaces.instMeasurableSpaceR = MeasurableSpace.comap QuasiBorelSpaces.R.val inferInstance

instance QuasiBorelSpaces.instMeasureSpaceR : MeasureTheory.MeasureSpace R

Pull back the Lebesgue measure along val

Equations

• QuasiBorelSpaces.instMeasureSpaceR = { toMeasurableSpace := QuasiBorelSpaces.instMeasurableSpaceR, volume := MeasureTheory.Measure.comap QuasiBorelSpaces.R.val MeasureTheory.volume }

instance QuasiBorelSpaces.instSigmaFiniteRVolume : MeasureTheory.SigmaFinite MeasureTheory.volume

instance QuasiBorelSpaces.instQuasiBorelSpaceR : QuasiBorelSpace R

Equations

• QuasiBorelSpaces.instQuasiBorelSpaceR = QuasiBorelSpace.ofMeasurableSpace

instance QuasiBorelSpaces.instPartialOrderR : PartialOrder R

Discrete order on the randomness carrier

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaCompletePartialOrderR : OmegaCompletePartialOrder R

Trivial ωCPO on R: chains are constant by discreteness

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaQuasiBorelSpaceR : OmegaQuasiBorelSpace R

ωQBS structure on R (compatibility axiom holds vacuously)

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaCompletePartialOrderENNReal : OmegaCompletePartialOrder ENNReal

ωCPO on extended non-negative reals using the usual supremum of a chain

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaQuasiBorelSpaceENNReal : OmegaQuasiBorelSpace ENNReal

ωQBS structure on ENNReal

Equations

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

instance QuasiBorelSpaces.instOmegaCompletePartialOrderUnit_quasiBorelSpaces : OmegaCompletePartialOrder Unit

Trivial ωQBS on the unit type

Equations

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

instance QuasiBorelSpaces.instOmegaQuasiBorelSpaceUnit : OmegaQuasiBorelSpace Unit

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaQuasiBorelSpaceOption (X : Type u_1) [OmegaQuasiBorelSpace X] : OmegaQuasiBorelSpace (Option X)

ωQBS structure on lifted values

Equations

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

@[reducible, inline]

abbrev QuasiBorelSpaces.RX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Randomizations of X are partial maps from the randomness source

Equations

• QuasiBorelSpaces.RX X = (QuasiBorelSpaces.R →ω𝒒 Option X)

@[reducible, inline]

abbrev QuasiBorelSpaces.JX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Expectation operators on X (the Giry-style exponential)

Equations

• QuasiBorelSpaces.JX X = ((X →ω𝒒 ENNReal) →ω𝒒 ENNReal)

def QuasiBorelSpaces.liftWeight (X : Type u_1) (w : X → ENNReal) : Option X → ENNReal

Lift a weight to a partial result

Equations

• QuasiBorelSpaces.liftWeight X w (some x_1) = w x_1
• QuasiBorelSpaces.liftWeight X w none = 0

def QuasiBorelSpaces.dom (X : Type u_1) [OmegaQuasiBorelSpace X] (α : RX X) : Set R

Domain of a randomization

Equations

• QuasiBorelSpaces.dom X α = {r : QuasiBorelSpaces.R | α r ≠ none}

def QuasiBorelSpaces.E_map (X : Type u_1) [OmegaQuasiBorelSpace X] (α : RX X) (w : X →ω𝒒 ENNReal) : ENNReal

Evaluate the expectation of a weight under a randomization

Equations

• QuasiBorelSpaces.E_map X α w = ∫⁻ (r : QuasiBorelSpaces.R), QuasiBorelSpaces.liftWeight X (fun (x : X) => w x) (α r)

def QuasiBorelSpaces.E_op (X : Type u_1) [OmegaQuasiBorelSpace X] (α : RX X) : JX X

Bundle the expectation operator arising from a randomization

Equations

• QuasiBorelSpaces.E_op X α = ⟨{ toFun := fun (w : X →ω𝒒 ENNReal) => QuasiBorelSpaces.E_map X α w, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

def QuasiBorelSpaces.E (X : Type u_1) [OmegaQuasiBorelSpace X] : RX X →ω𝒒 JX X

The expectation morphism E : RX → JX

Equations

• QuasiBorelSpaces.E X = ⟨{ toFun := fun (α : QuasiBorelSpaces.RX X) => QuasiBorelSpaces.E_op X α, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

def QuasiBorelSpaces.return_R (X : Type u_1) [OmegaQuasiBorelSpace X] (x : X) : RX X

Monad unit on randomizations (Dirac)

Equations

• QuasiBorelSpaces.return_R X x = ⟨{ toFun := fun (r : QuasiBorelSpaces.R) => if r.val ∈ Set.Icc 0 1 then some x else none, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

class QuasiBorelSpaces.RandomSplit : Type

A measurable splitting of randomness as in the transfer principle

• φ : R → R × R

  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

noncomputable instance QuasiBorelSpaces.defaultRandomSplit : RandomSplit

A default instance of RandomSplit (placeholder for now)

Equations

• QuasiBorelSpaces.defaultRandomSplit = { φ := sorry, measurable_φ := QuasiBorelSpaces.defaultRandomSplit._proof_1, preserves_volume := QuasiBorelSpaces.defaultRandomSplit._proof_2 }

def QuasiBorelSpaces.bind_R (X : Type u_1) [OmegaQuasiBorelSpace X] [RandomSplit] {Y : Type u_1} [OmegaQuasiBorelSpace Y] (α : RX X) (k : X → RX Y) : RX Y

Monad bind on randomizations using the randomness splitting

Equations

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

def QuasiBorelSpaces.return_J (X : Type u_1) [OmegaQuasiBorelSpace X] (x : X) : JX X

Monad unit on expectation operators

Equations

• QuasiBorelSpaces.return_J X x = ⟨{ toFun := fun (w : X →ω𝒒 ENNReal) => w x, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

def QuasiBorelSpaces.bind_J (X : Type u_1) [OmegaQuasiBorelSpace X] {Y : Type u_2} [OmegaQuasiBorelSpace Y] (μ : JX X) (k : X → JX Y) : JX Y

Monad bind on expectation operators

Equations

• QuasiBorelSpaces.bind_J X μ k = ⟨{ toFun := fun (w : Y →ω𝒒 ENNReal) => μ ⟨{ toFun := fun (x : X) => (k x) w, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

theorem QuasiBorelSpaces.return_bind_J (X : Type u_1) [OmegaQuasiBorelSpace X] {Y : Type u_2} [OmegaQuasiBorelSpace Y] {x : X} {f : X → JX Y} : bind_J X (return_J X x) f = f x

theorem QuasiBorelSpaces.bind_return_J (X : Type u_1) [OmegaQuasiBorelSpace X] {Y : Type u_2} [OmegaQuasiBorelSpace Y] {x : JX X} : bind_J X x (return_J X) = x

theorem QuasiBorelSpaces.bind_bind_J (X : Type u_1) [OmegaQuasiBorelSpace X] {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] {x : JX X} {f : X → JX Y} {g : Y → JX Z} : bind_J Y (bind_J X x f) g = bind_J X x fun (y : X) => bind_J Y (f y) g

theorem QuasiBorelSpaces.E_preserves_return (X : Type u_1) [OmegaQuasiBorelSpace X] (x : X) : (E X) (return_R X x) = return_J X x

Expectation preserves the monad structure on randomizations

theorem QuasiBorelSpaces.E_preserves_bind (X : Type u_1) [OmegaQuasiBorelSpace X] {Y : Type u_1} [OmegaQuasiBorelSpace Y] (α : RX X) (k : X →ω𝒒 RX Y) : (E Y) (bind_R X α ⇑k) = bind_J X ((E X) α) fun (x : X) => (E Y) (k x)

def QuasiBorelSpaces.Randomizable (X : Type u_1) [OmegaQuasiBorelSpace X] (μ : JX X) : Prop

Predicate: expectation operator arising from a randomization

Equations

• QuasiBorelSpaces.Randomizable X μ = ∃ (α : QuasiBorelSpaces.RX X), μ = QuasiBorelSpaces.E_op X α

def QuasiBorelSpaces.SX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Randomizable expectation operators as a subtype

Equations

• QuasiBorelSpaces.SX X = { μ : QuasiBorelSpaces.JX X // QuasiBorelSpaces.Randomizable X μ }

@[reducible, inline]

abbrev QuasiBorelSpaces.MRX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Randomizations valued in randomizations

Equations

• QuasiBorelSpaces.MRX X = (QuasiBorelSpaces.R →ω𝒒 QuasiBorelSpaces.RX X)

@[reducible, inline]

abbrev QuasiBorelSpaces.MSX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Randomizable random operators (random elements of JX)

Equations

• QuasiBorelSpaces.MSX X = (QuasiBorelSpaces.R →ω𝒒 QuasiBorelSpaces.JX X)

noncomputable def QuasiBorelSpaces.E_rand (X : Type u_1) [OmegaQuasiBorelSpace X] (β : MRX X) : MSX X

Extend E pointwise to random randomizations

Equations

• QuasiBorelSpaces.E_rand X β = ⟨{ toFun := fun (r : QuasiBorelSpaces.R) => QuasiBorelSpaces.E_op X (β r), monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

inductive QuasiBorelSpaces.InTX (X : Type u_1) [OmegaQuasiBorelSpace X] : JX X → Prop

Membership in the ω-sup-closure of randomizable operators

• randomizable {X : Type u_1} [OmegaQuasiBorelSpace X] (α : RX X) : InTX X (E_op X α)

  Randomizable operators are in the closure

• sup {X : Type u_1} [OmegaQuasiBorelSpace X] {c : OmegaCompletePartialOrder.Chain (JX X)} : (∀ (n : ℕ), InTX X (c n)) → InTX X (OmegaCompletePartialOrder.ωSup c)

  The closure is closed under ω-sups

inductive QuasiBorelSpaces.InMTX (X : Type u_1) [OmegaQuasiBorelSpace X] : MSX X → Prop

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

• randomizable {X : Type u_1} [OmegaQuasiBorelSpace X] (β : MRX X) : InMTX X (E_rand X β)

  Randomizable random operators are in the closure

• sup {X : Type u_1} [OmegaQuasiBorelSpace X] {c : OmegaCompletePartialOrder.Chain (MSX X)} : (∀ (n : ℕ), InMTX X (c n)) → InMTX X (OmegaCompletePartialOrder.ωSup c)

  The closure is closed under ω-sups

@[reducible, inline]

abbrev QuasiBorelSpaces.TX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Probabilistic powerdomain: smallest ω-subcpo of JX

Equations

• QuasiBorelSpaces.TX X = { μ : QuasiBorelSpaces.JX X // QuasiBorelSpaces.InTX X μ }

@[reducible, inline]

abbrev QuasiBorelSpaces.MTX (X : Type u_1) [OmegaQuasiBorelSpace X] : Type u_1

Random elements of the powerdomain

Equations

• QuasiBorelSpaces.MTX X = { β : QuasiBorelSpaces.MSX X // QuasiBorelSpaces.InMTX X β }

noncomputable instance QuasiBorelSpaces.instPartialOrderTX (X : Type u_1) [OmegaQuasiBorelSpace X] : PartialOrder (TX X)

Order structure on T X inherited from the ambient JX

Equations

• QuasiBorelSpaces.instPartialOrderTX X = inferInstance

noncomputable instance QuasiBorelSpaces.instPartialOrderMTX (X : Type u_1) [OmegaQuasiBorelSpace X] : PartialOrder (MTX X)

Order structure on M T X inherited from the ambient M JX

Equations

• QuasiBorelSpaces.instPartialOrderMTX X = inferInstance

def QuasiBorelSpaces.TX.incl (X : Type u_1) [OmegaQuasiBorelSpace X] (t : TX X) : JX X

Inclusion of TX into JX

Equations

• QuasiBorelSpaces.TX.incl X t = ↑t

def QuasiBorelSpaces.MTX.incl (X : Type u_1) [OmegaQuasiBorelSpace X] (t : MTX X) : MSX X

Inclusion of MTX into MSX

Equations

• QuasiBorelSpaces.MTX.incl X t = ↑t

noncomputable def QuasiBorelSpaces.E_T (X : Type u_1) [OmegaQuasiBorelSpace X] (α : RX X) : TX X

Expectation factors through T

Equations

• QuasiBorelSpaces.E_T X α = ⟨QuasiBorelSpaces.E_op X α, ⋯⟩

noncomputable def QuasiBorelSpaces.E_MT (X : Type u_1) [OmegaQuasiBorelSpace X] (β : MRX X) : MTX X

Pointwise extension of E_T to random randomizations

Equations

• QuasiBorelSpaces.E_MT X β = ⟨QuasiBorelSpaces.E_rand X β, ⋯⟩

noncomputable instance QuasiBorelSpaces.instOmegaCompletePartialOrderTX (X : Type u_1) [OmegaQuasiBorelSpace X] : OmegaCompletePartialOrder (TX X)

TX inherits an ωCPO structure from JX

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaQuasiBorelSpaceTX (X : Type u_1) [OmegaQuasiBorelSpace X] : OmegaQuasiBorelSpace (TX X)

TX is an ωQBS as a full subobject of JX

Equations

• QuasiBorelSpaces.instOmegaQuasiBorelSpaceTX X = { toOmegaCompletePartialOrder := inferInstance, toQuasiBorelSpace := inferInstance, isHom_ωSup := ⋯ }

noncomputable instance QuasiBorelSpaces.instOmegaCompletePartialOrderMTX (X : Type u_1) [OmegaQuasiBorelSpace X] : OmegaCompletePartialOrder (MTX X)

MTX inherits an ωCPO structure from MSX

Equations

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

noncomputable instance QuasiBorelSpaces.instOmegaQuasiBorelSpaceMTX (X : Type u_1) [OmegaQuasiBorelSpace X] : OmegaQuasiBorelSpace (MTX X)

MTX is an ωQBS as a full subobject of MSX

Equations

• QuasiBorelSpaces.instOmegaQuasiBorelSpaceMTX X = { toOmegaCompletePartialOrder := inferInstance, toQuasiBorelSpace := inferInstance, isHom_ωSup := ⋯ }

def QuasiBorelSpaces.return_T (X : Type u_1) [OmegaQuasiBorelSpace X] (x : X) : TX X

Monad unit on T obtained by restriction

Equations

• QuasiBorelSpaces.return_T X x = ⟨QuasiBorelSpaces.return_J X x, ⋯⟩

def QuasiBorelSpaces.bind_T (X : Type u_1) [OmegaQuasiBorelSpace X] {Y : Type u_2} [OmegaQuasiBorelSpace Y] (t : TX X) (k : X → TX Y) : TX Y

Monad bind on T, restricting the J bind

Equations

• QuasiBorelSpaces.bind_T X t k = ⟨QuasiBorelSpaces.bind_J X ↑t fun (x : X) => ↑(k x), ⋯⟩

theorem QuasiBorelSpaces.expectation_factorizes_monad : True

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

noncomputable def QuasiBorelSpaces.sample_map : Unit → RX R

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 QuasiBorelSpaces.score_map (r : R) : RX Unit

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

Equations

• QuasiBorelSpaces.score_map r = ⟨{ toFun := fun (t : QuasiBorelSpaces.R) => if t.val ∈ Set.Icc 0 |r.val| then some () else none, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

noncomputable def QuasiBorelSpaces.sample_T : Unit → TX R

Sampling lifted to the powerdomain

Equations

• QuasiBorelSpaces.sample_T x✝ = QuasiBorelSpaces.E_T QuasiBorelSpaces.R (QuasiBorelSpaces.sample_map ())

noncomputable def QuasiBorelSpaces.score_T (r : R) : TX Unit

Conditioning lifted to the powerdomain

Equations

• QuasiBorelSpaces.score_T r = QuasiBorelSpaces.E_T Unit (QuasiBorelSpaces.score_map r)