Probability Measures over Quasi-Borel Spaces

This file defines probability measures over quasi-borel spaces.

See [HKSY17], Section V-D.

Basic Definitions

structure QuasiBorelSpace.ProbabilityMeasure (A : Type u_7) [QuasiBorelSpace A] : Type u_7

The type of (quasi-borel) probability measures.

• fromQuotient :: (
• val : Quotient (QuasiBorelSpace.PreProbabilityMeasure.setoid A)
• )

def QuasiBorelSpace.ProbabilityMeasure.mk {A : Type u_1} [QuasiBorelSpace A] (μ : PreProbabilityMeasure A) : ProbabilityMeasure A

Constructs a ProbabilityMeasure from a PreProbabilityMeasure.

Equations

• QuasiBorelSpace.ProbabilityMeasure.mk μ = { val := ⟦μ⟧ }

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.mk_eq_iff {A : Type u_1} [QuasiBorelSpace A] (μ ν : PreProbabilityMeasure A) : mk μ = mk ν ↔ μ ≈ ν

Two ProbabilityMeasures are equal iff their underlying PreProbabilityMeasures are equivalent.

theorem QuasiBorelSpace.ProbabilityMeasure.inductionOn {A : Type u_1} [QuasiBorelSpace A] {motive : ProbabilityMeasure A → Prop} (μ : ProbabilityMeasure A) (mk : ∀ (μ : PreProbabilityMeasure A), motive (mk μ)) : motive μ

Induction principle for ProbabilityMeasure.

noncomputable def QuasiBorelSpace.ProbabilityMeasure.toPreProbabilityMeasure {A : Type u_1} [QuasiBorelSpace A] (μ : ProbabilityMeasure A) : PreProbabilityMeasure A

Converts a ProbabilityMeasure to the underlying PreProbabilityMeasure. This may or may not be the one passed to mk, but will always be equivalent ((mk μ).toPreProbabilityMeasure ≈ μ).

Equations

• μ.toPreProbabilityMeasure = (QuasiBorelSpace.ProbabilityMeasure.val✝ μ).out

theorem QuasiBorelSpace.ProbabilityMeasure.toPreProbabilityMeasure_mk {A : Type u_1} [QuasiBorelSpace A] (μ : PreProbabilityMeasure A) : (mk μ).toPreProbabilityMeasure ≈ μ

theorem QuasiBorelSpace.ProbabilityMeasure.nonempty {A : Type u_1} [QuasiBorelSpace A] (μ : ProbabilityMeasure A) : Nonempty A

Every ProbabilityMeasure has a nonempty carrier.

QuasiBorelSpace Instance

instance QuasiBorelSpace.ProbabilityMeasure.inst {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (ProbabilityMeasure A)

The QuasiBorelSpace structure on ProbabilityMeasure A.

Equations

• QuasiBorelSpace.ProbabilityMeasure.inst = QuasiBorelSpace.lift QuasiBorelSpace.ProbabilityMeasure.toPreProbabilityMeasure

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_toPreProbabilityMeasure {A : Type u_1} [QuasiBorelSpace A] : IsHom toPreProbabilityMeasure

toPreProbabilityMeasure is a homomorphism.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_mk {A : Type u_1} [QuasiBorelSpace A] : IsHom mk

mk is a homomorphism.

Integrals

noncomputable def QuasiBorelSpace.ProbabilityMeasure.lintegral {A : Type u_1} [QuasiBorelSpace A] (k : A → ENNReal) (μ : ProbabilityMeasure A) : ENNReal

The integral of a function over a ProbabilityMeasure.

Equations

• QuasiBorelSpace.ProbabilityMeasure.lintegral k μ = QuasiBorelSpace.PreProbabilityMeasure.lintegral k μ.toPreProbabilityMeasure

def QuasiBorelSpace.ProbabilityMeasure.«term∫⁻_,_∂_» : Lean.ParserDescr

The integral of a function over a ProbabilityMeasure.

Equations

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mk {A : Type u_1} [QuasiBorelSpace A] {k : A → ENNReal} (hk : IsHom k) (μ : PreProbabilityMeasure A) : lintegral (fun (x : A) => k x) (mk μ) = PreProbabilityMeasure.lintegral k μ

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_toPreProbabilityMeasure {A : Type u_1} [QuasiBorelSpace A] (μ : ProbabilityMeasure A) (k : A → ENNReal) : PreProbabilityMeasure.lintegral k μ.toPreProbabilityMeasure = lintegral (fun (x : A) => k x) μ

Converting to PreProbabilityMeasure and back preserves the integral.

theorem QuasiBorelSpace.ProbabilityMeasure.ext {A : Type u_1} [QuasiBorelSpace A] {μ₁ μ₂ : ProbabilityMeasure A} (hμ : ∀ {k : A → ENNReal}, IsHom k → lintegral (fun (x : A) => k x) μ₁ = lintegral (fun (x : A) => k x) μ₂) : μ₁ = μ₂

Two ProbabilityMeasures are equal iff they have the same integrals.

theorem QuasiBorelSpace.ProbabilityMeasure.ext_iff {A : Type u_1} [QuasiBorelSpace A] {μ₁ μ₂ : ProbabilityMeasure A} : μ₁ = μ₂ ↔ ∀ {k : A → ENNReal}, IsHom k → lintegral (fun (x : A) => k x) μ₁ = lintegral (fun (x : A) => k x) μ₂

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_lintegral {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {k : A → B → ENNReal} (hk : IsHom fun (x : A × B) => match x with | (x, y) => k x y) {f : A → ProbabilityMeasure B} (hf : IsHom f) : IsHom fun (x : A) => lintegral (fun (y : B) => k x y) (f x)

The integral of a homomorphism is itself a homomorphism.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_add_left {A : Type u_1} [QuasiBorelSpace A] {f : A → ENNReal} (hf : IsHom f) (g : A → ENNReal) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => f x + g x) μ = lintegral (fun (x : A) => f x) μ + lintegral (fun (x : A) => g x) μ

Linearity of integration: addition on the left.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_add_right {A : Type u_1} [QuasiBorelSpace A] (f : A → ENNReal) {g : A → ENNReal} (hg : IsHom g) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => f x + g x) μ = lintegral (fun (x : A) => f x) μ + lintegral (fun (x : A) => g x) μ

Linearity of integration: addition on the right.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mul_left {A : Type u_1} [QuasiBorelSpace A] (c : ENNReal) {f : A → ENNReal} (hf : IsHom f) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => c * f x) μ = c * lintegral (fun (x : A) => f x) μ

Linearity of integration: scalar multiplication on the left.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mul_right {A : Type u_1} [QuasiBorelSpace A] (c : ENNReal) {f : A → ENNReal} (hf : IsHom f) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => f x * c) μ = lintegral (fun (x : A) => f x) μ * c

Linearity of integration: scalar multiplication on the right.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_const {A : Type u_1} [QuasiBorelSpace A] (c : ENNReal) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => c) μ = c

The integral of a constant function is the constant.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mono {A : Type u_1} [QuasiBorelSpace A] {f g : A → ENNReal} (h : f ≤ g) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => f x) μ ≤ lintegral (fun (x : A) => g x) μ

Monotonicity of integration.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_iSup {A : Type u_1} [QuasiBorelSpace A] (f : ℕ → A → ENNReal) (hf₁ : Monotone f) (hf₂ : ∀ (n : ℕ), IsHom (f n)) (μ : ProbabilityMeasure A) : ⨆ (n : ℕ), lintegral (fun (x : A) => f n x) μ = lintegral (fun (x : A) => ⨆ (n : ℕ), f n x) μ

Monotone convergence theorem for integrals.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_finset_sum {B : Type u_2} [QuasiBorelSpace B] {A : Type u_7} (s : Finset A) {f : A → B → ENNReal} (hf : ∀ b ∈ s, IsHom (f b)) (μ : ProbabilityMeasure B) : lintegral (fun (a : B) => ∑ b ∈ s, f b a) μ = ∑ b ∈ s, lintegral (fun (a : B) => f b a) μ

The integral of a finite sum is the sum of the integrals.

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_sub_le {A : Type u_1} [QuasiBorelSpace A] (f : A → ENNReal) {g : A → ENNReal} (hg : IsHom g) (μ : ProbabilityMeasure A) : lintegral (fun (x : A) => f x) μ - lintegral (fun (x : A) => g x) μ ≤ lintegral (fun (x : A) => f x - g x) μ

Upper bound for subtraction of integrals.

Measures

noncomputable instance QuasiBorelSpace.ProbabilityMeasure.instFunLikeSetENNReal {A : Type u_1} [QuasiBorelSpace A] : FunLike (ProbabilityMeasure A) (Set A) ENNReal

The FunLike instance for ProbabilityMeasure.

Equations

• QuasiBorelSpace.ProbabilityMeasure.instFunLikeSetENNReal = { coe := fun (μ : QuasiBorelSpace.ProbabilityMeasure A) (s : Set A) => μ.toPreProbabilityMeasure.measureOf s, coe_injective' := ⋯ }

instance QuasiBorelSpace.ProbabilityMeasure.instOuterMeasureClass {A : Type u_1} [QuasiBorelSpace A] : MeasureTheory.OuterMeasureClass (ProbabilityMeasure A) A

The OuterMeasureClass instance for ProbabilityMeasure.

Point Separation

instance QuasiBorelSpace.ProbabilityMeasure.instSeparatesPoints {A : Type u_1} [QuasiBorelSpace A] : SeparatesPoints (ProbabilityMeasure A)

The SeparatesPoints instance for ProbabilityMeasure.

Operations

unit

noncomputable def QuasiBorelSpace.ProbabilityMeasure.unit {A : Type u_1} [QuasiBorelSpace A] (x : A) : ProbabilityMeasure A

The monadic unit operation.

Equations

• QuasiBorelSpace.ProbabilityMeasure.unit x = QuasiBorelSpace.ProbabilityMeasure.mk (QuasiBorelSpace.PreProbabilityMeasure.unit x)

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_unit {A : Type u_1} [QuasiBorelSpace A] : IsHom unit

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_unit {A : Type u_1} [QuasiBorelSpace A] {k : A → ENNReal} (hk : IsHom k) (x : A) : lintegral (fun (x : A) => k x) (unit x) = k x

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.unit_injective {A : Type u_1} [QuasiBorelSpace A] [SeparatesPoints A] : Function.Injective unit

unit is injective when the carrier separates points.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.unit_inj {A : Type u_1} [QuasiBorelSpace A] [SeparatesPoints A] (x y : A) : unit x = unit y ↔ x = y

unit is injective iff the inputs are equal.

theorem QuasiBorelSpace.ProbabilityMeasure.separatesPoints_iff_unit_injective {A : Type u_1} [QuasiBorelSpace A] : SeparatesPoints A ↔ Function.Injective unit

A separates points iff unit is injective.

bind

noncomputable def QuasiBorelSpace.ProbabilityMeasure.bind {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A → ProbabilityMeasure B) (μ : ProbabilityMeasure A) : ProbabilityMeasure B

The monadic bind operation.

Equations

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_bind {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → ProbabilityMeasure B} (hf : IsHom f) : IsHom (bind f)

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_bind {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {k : B → ENNReal} (hk : IsHom k) {f : A → ProbabilityMeasure B} (hf : IsHom f) (μ : ProbabilityMeasure A) : lintegral (fun (x : B) => k x) (bind f μ) = lintegral (fun (x : A) => lintegral (fun (y : B) => k y) (f x)) μ

Computing the integral of bind.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.bind_unit {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → ProbabilityMeasure B} (hf : IsHom f) (x : A) : bind f (unit x) = f x

Left unit law for bind.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.unit_bind {A : Type u_1} [QuasiBorelSpace A] (μ : ProbabilityMeasure A) : bind unit μ = μ

Right unit law for bind.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.bind_bind {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : B → ProbabilityMeasure C} (hf : IsHom f) {g : A → ProbabilityMeasure B} (hg : IsHom g) (μ : ProbabilityMeasure A) : bind f (bind g μ) = bind (fun (x : A) => bind f (g x)) μ

Associativity of bind.

map

noncomputable def QuasiBorelSpace.ProbabilityMeasure.map {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A → B) (μ : ProbabilityMeasure A) : ProbabilityMeasure B

The functorial map operation.

Equations

• QuasiBorelSpace.ProbabilityMeasure.map f μ = QuasiBorelSpace.ProbabilityMeasure.bind (fun (x : A) => QuasiBorelSpace.ProbabilityMeasure.unit (f x)) μ

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_map {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) : IsHom (map f)

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_map {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {k : B → ENNReal} (hk : IsHom k) {f : A → B} (hf : IsHom f) (μ : ProbabilityMeasure A) : lintegral (fun (x : B) => k x) (map f μ) = lintegral (fun (x : A) => k (f x)) μ

Computing the integral of map.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_id {A : Type u_1} [QuasiBorelSpace A] : (map fun (x : A) => x) = id

map of the identity function is the identity.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_id' {A : Type u_1} [QuasiBorelSpace A] : map id = id

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_map {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : B → C} (hf : IsHom f) {g : A → B} (hg : IsHom g) (μ : ProbabilityMeasure A) : map f (map g μ) = map (fun (x : A) => f (g x)) μ

Functor composition law for map.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_bind {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : B → C} (hf : IsHom f) {g : A → ProbabilityMeasure B} (hg : IsHom g) (μ : ProbabilityMeasure A) : map f (bind g μ) = bind (fun (x : A) => map f (g x)) μ

Commutation of map and bind.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.bind_map {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : B → ProbabilityMeasure C} (hf : IsHom f) {g : A → B} (hg : IsHom g) (μ : ProbabilityMeasure A) : bind f (map g μ) = bind (fun (x : A) => f (g x)) μ

Commutation of bind and map.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_unit {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) (x : A) : map f (unit x) = unit (f x)

map commutes with unit.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.bind_unit_eq_map {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} : (bind fun (x : A) => unit (f x)) = map f

bind with unit is equivalent to map.

str

noncomputable def QuasiBorelSpace.ProbabilityMeasure.str {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (x : A) (μ : ProbabilityMeasure B) : ProbabilityMeasure (A × B)

The functorial strength operation.

Equations

• QuasiBorelSpace.ProbabilityMeasure.str x μ = QuasiBorelSpace.ProbabilityMeasure.mk (QuasiBorelSpace.PreProbabilityMeasure.str x μ.toPreProbabilityMeasure)

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_str {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {k : A × B → ENNReal} (hk : IsHom k) (x : A) (μ : ProbabilityMeasure B) : lintegral (fun (p : A × B) => k p) (str x μ) = lintegral (fun (y : B) => k (x, y)) μ

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_str {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] : IsHom (Function.uncurry str)

str is a homomorphism in both arguments.

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_str' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A → B} (hf : IsHom f) {g : A → ProbabilityMeasure C} (hg : IsHom g) : IsHom fun (x : A) => str (f x) (g x)

str is a homomorphism when composed with other homomorphisms.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.str_eq_map {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (x : A) (μ : ProbabilityMeasure B) : str x μ = map (fun (x_1 : B) => (x, x_1)) μ

str expressed in terms of map.

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_bind' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : C → A → ProbabilityMeasure B} (hf : IsHom (Function.uncurry f)) {g : C → ProbabilityMeasure A} (hg : IsHom g) : IsHom fun (x : C) => bind (f x) (g x)

Helper lemma for proving bind is a homomorphism with uncurried functions.

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_map' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : C → A → B} (hf : IsHom (Function.uncurry f)) {g : C → ProbabilityMeasure A} (hg : IsHom g) : IsHom fun (x : C) => map (f x) (g x)

Helper lemma for proving map is a homomorphism with uncurried functions.

coin

noncomputable def QuasiBorelSpace.ProbabilityMeasure.coin (p : ↑unitInterval) : ProbabilityMeasure Bool

The Bernoulli measure.

Equations

• QuasiBorelSpace.ProbabilityMeasure.coin p = QuasiBorelSpace.ProbabilityMeasure.mk (QuasiBorelSpace.PreProbabilityMeasure.coin p)

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_coin (k : Bool → ENNReal) (p : ↑unitInterval) : lintegral (fun (x : Bool) => k x) (coin p) = ENNReal.ofReal ↑p * k true + ENNReal.ofReal (1 - ↑p) * k false

choose

noncomputable def QuasiBorelSpace.ProbabilityMeasure.choose {A : Type u_1} [QuasiBorelSpace A] (p : ↑unitInterval) (μ ν : ProbabilityMeasure A) : ProbabilityMeasure A

Probabilistic choice.

Equations

• QuasiBorelSpace.ProbabilityMeasure.choose p μ ν = QuasiBorelSpace.ProbabilityMeasure.bind (fun (b : Bool) => if b = true then μ else ν) (QuasiBorelSpace.ProbabilityMeasure.coin p)

def QuasiBorelSpace.ProbabilityMeasure.«term_◃_▹_» : Lean.TrailingParserDescr

Probabilistic choice.

Equations

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

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_choose {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (p : ↑unitInterval) {f : A → ProbabilityMeasure B} (hf : IsHom f) {g : A → ProbabilityMeasure B} (hg : IsHom g) : IsHom fun (x : A) => choose p (f x) (g x)

choose is a homomorphism.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_choose {A : Type u_1} [QuasiBorelSpace A] {k : A → ENNReal} (hk : IsHom k) (p : ↑unitInterval) (μ ν : ProbabilityMeasure A) : lintegral (fun (x : A) => k x) (choose p μ ν) = ENNReal.ofReal ↑p * lintegral (fun (x : A) => k x) μ + ENNReal.ofReal ↑(unitInterval.symm p) * lintegral (fun (x : A) => k x) ν

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.choose_one {A : Type u_1} [QuasiBorelSpace A] (μ ν : ProbabilityMeasure A) : choose 1 μ ν = μ

Choosing with probability 1 returns the first measure.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.choose_zero {A : Type u_1} [QuasiBorelSpace A] (μ ν : ProbabilityMeasure A) : choose 0 μ ν = ν

Choosing with probability 0 returns the second measure.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.choose_eq {A : Type u_1} [QuasiBorelSpace A] (p : ↑unitInterval) (μ : ProbabilityMeasure A) : choose p μ μ = μ

Choosing between the same measure returns the measure.

theorem QuasiBorelSpace.ProbabilityMeasure.choose_comm {A : Type u_1} [QuasiBorelSpace A] (p : ↑unitInterval) (μ ν : ProbabilityMeasure A) : choose p μ ν = choose (unitInterval.symm p) ν μ

choose is commutative with symmetric probabilities.

theorem QuasiBorelSpace.ProbabilityMeasure.choose_assoc {A : Type u_1} [QuasiBorelSpace A] {p q : ↑unitInterval} {μ₁ μ₂ μ₃ : ProbabilityMeasure A} : choose q (choose p μ₁ μ₂) μ₃ = choose (p * q) μ₁ (choose (unitInterval.assocProd p q) μ₂ μ₃)

Associativity of choose with appropriate probability adjustments.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.bind_choose {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → ProbabilityMeasure B} (hf : IsHom f) (p : ↑unitInterval) (μ ν : ProbabilityMeasure A) : bind f (choose p μ ν) = choose p (bind f μ) (bind f ν)

bind distributes over choose.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_choose {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) (p : ↑unitInterval) (μ ν : ProbabilityMeasure A) : map f (choose p μ ν) = choose p (map f μ) (map f ν)

map distributes over choose.

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.choose_bind {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → ProbabilityMeasure B} (hf : IsHom f) {g : A → ProbabilityMeasure B} (hg : IsHom g) (p : ↑unitInterval) (μ : ProbabilityMeasure A) : bind (fun (x : A) => choose p (f x) (g x)) μ = choose p (bind f μ) (bind g μ)

choose commutes with bind.

Order Structure

instance QuasiBorelSpace.instPartialOrderProbabilityMeasure {A : Type u_1} [QuasiBorelSpace A] : PartialOrder (ProbabilityMeasure A)

the discrete order on ProbabilityMeasure

Equations

• QuasiBorelSpace.instPartialOrderProbabilityMeasure = { le := fun (x y : QuasiBorelSpace.ProbabilityMeasure A) => x = y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

instance QuasiBorelSpace.instOmegaCompletePartialOrderProbabilityMeasure {A : Type u_1} [QuasiBorelSpace A] : OmegaCompletePartialOrder (ProbabilityMeasure A)

ProbabilityMeasure is an ωCPO with the discrete order

Equations

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