Probability Measures on Quasi-Borel Spaces

This file defines monadic operations on quasi-Borel spaces.

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_id {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A → A} (hf : ∀ (x : A), f x = x) : map f = id

@[simp]

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

pure

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

Equations

• QuasiBorelSpace.ProbabilityMeasure.pure x = QuasiBorelSpace.ProbabilityMeasure.mk { toFun := fun (x_1 : ↑unitInterval) => x, property := ⋯ }

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_pure {A : Type u_1} {x✝ : QuasiBorelSpace A} : IsHom pure

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_pure {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A → ENNReal} (hf : IsHom f) (x : A) : lintegral f (pure x) = f x

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_pure {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {f : A → B} (hf : IsHom f) (x : A) : map f (pure x) = pure (f x)

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)

Equations

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

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_str {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {f : A × B → ENNReal} (hf : IsHom f) (x : A) (μ : ProbabilityMeasure B) : lintegral f (str x μ) = lintegral (fun (y : B) => f (x, y)) μ

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_str {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} : IsHom fun (x : A × ProbabilityMeasure B) => str x.1 x.2

@[simp]

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_map' {A : Type u_2} {B : Type u_1} {C : Type u_3} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : QuasiBorelSpace C} {g : A → ProbabilityMeasure B} {f : A → B → C} (hf : IsHom fun (x : A × B) => f x.1 x.2) (hg : IsHom g) : IsHom fun (x : A) => map (f x) (g x)

join

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

Equations

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_join {A : Type u_1} {x✝ : QuasiBorelSpace A} : IsHom join

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_join {A : Type u_1} {x✝ : QuasiBorelSpace A} (k : A → ENNReal) (hk : IsHom k) (μ : ProbabilityMeasure (ProbabilityMeasure A)) : lintegral k μ.join = lintegral (lintegral k) μ

theorem QuasiBorelSpace.ProbabilityMeasure.map_join {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {f : A → B} (hf : IsHom f) (μ : ProbabilityMeasure (ProbabilityMeasure A)) : map f μ.join = (map (map f) μ).join

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.join_pure {A : Type u_1} {x✝ : QuasiBorelSpace A} (μ : ProbabilityMeasure A) : (pure μ).join = μ

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.join_map_pure {A : Type u_1} {x✝ : QuasiBorelSpace A} (μ : ProbabilityMeasure A) : (map pure μ).join = μ

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.join_map_join {A : Type u_1} {x✝ : QuasiBorelSpace A} (μ : ProbabilityMeasure (ProbabilityMeasure (ProbabilityMeasure A))) : (map join μ).join = μ.join.join

bind

noncomputable def QuasiBorelSpace.ProbabilityMeasure.bind {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} (f : A → ProbabilityMeasure B) (μ : ProbabilityMeasure A) : ProbabilityMeasure B

Equations

• QuasiBorelSpace.ProbabilityMeasure.bind f μ = (QuasiBorelSpace.ProbabilityMeasure.map f μ).join

@[simp]

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.isHom_bind {A : Type u_3} {B : Type u_2} {C : Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : QuasiBorelSpace C} {f : A → B → ProbabilityMeasure C} {g : A → ProbabilityMeasure B} (hf : IsHom fun (x : A × B) => f x.1 x.2) (hg : IsHom g) : IsHom fun (x : A) => bind (f x) (g x)

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.pure_bind {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {f : A → B} (hf : IsHom f) : (bind fun (x : A) => pure (f x)) = map f

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.bind_pure {A : Type u_2} {B : Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {f : A → ProbabilityMeasure B} (hf : IsHom f) (x : A) : bind f (pure x) = f x

@[simp]

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

theorem QuasiBorelSpace.ProbabilityMeasure.bind_comm {A : Type u_3} {B : Type u_2} {C : Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : QuasiBorelSpace C} {f : A → B → ProbabilityMeasure C} (hf : IsHom fun (x : A × B) => f x.1 x.2) (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure B) : bind (fun (a : A) => bind (f a) ν) μ = bind (fun (a : B) => bind (fun (x : A) => f x a) μ) ν

@[simp]

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.map_bind {A : Type u_3} {B : Type u_1} {C : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : 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)) μ

uniform

noncomputable def QuasiBorelSpace.ProbabilityMeasure.uniform : ProbabilityMeasure ↑unitInterval

Equations

• QuasiBorelSpace.ProbabilityMeasure.uniform = QuasiBorelSpace.ProbabilityMeasure.mk QuasiBorelHom.id

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_uniform {k : ↑unitInterval → ENNReal} (hk : IsHom k) : lintegral k uniform = ∫⁻ (x : ↑unitInterval), k x

bernoulli

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

Equations

• QuasiBorelSpace.ProbabilityMeasure.bernoulli p = QuasiBorelSpace.ProbabilityMeasure.map (fun (i : ↑unitInterval) => decide (i < p)) QuasiBorelSpace.ProbabilityMeasure.uniform

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_bernoulli {k : Bool → ENNReal} (hk : IsHom k) (p : ↑unitInterval) : lintegral k (bernoulli p) = ENNReal.ofReal ↑p * k true + ENNReal.ofReal ↑(unitInterval.symm p) * k false

choose

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

Equations

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

@[simp]

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

@[simp]

theorem QuasiBorelSpace.ProbabilityMeasure.choose_id {A : Type u_1} {x✝ : QuasiBorelSpace A} {p : ↑unitInterval} (μ : ProbabilityMeasure A) : choose p μ μ = μ

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

@[simp]

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

@[simp]

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