LeanPool.QuasiBorelSpaces.PreProbabilityMeasure

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.PreProbabilityMeasure.

structure QuasiBorelSpace.PreProbabilityMeasure (A : Type u_5) [QuasiBorelSpace A] : Type u_5

A precursor to the type of probability measures. Intuitively, a (quasi-borel) probability measure is just a variable applied to a normal probability measure on ℝ. A PreProbabilityMeasure holds the underlying variable and probability measure.

• eval : ℝ →𝒒 A

  The random variable associated with the probability measure.

• base : MeasureTheory.ProbabilityMeasure ℝ

  The base ProbabilityMeasure.

theorem QuasiBorelSpace.PreProbabilityMeasure.ext {A : Type u_5} {inst✝ : QuasiBorelSpace A} {x y : PreProbabilityMeasure A} (eval : x.eval = y.eval) (base : x.base = y.base) : x = y

theorem QuasiBorelSpace.PreProbabilityMeasure.ext_iff {A : Type u_5} {inst✝ : QuasiBorelSpace A} {x y : PreProbabilityMeasure A} : x = y ↔ x.eval = y.eval ∧ x.base = y.base

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.lintegral {A : Type u_1} [QuasiBorelSpace A] (f : A → ENNReal) : PreProbabilityMeasure A → ENNReal

The integral of a function relative to a probability measure.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.lintegral f { eval := φ, base := μ } = ∫⁻ (x : ℝ), f (φ x) ∂↑μ

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_mk {A : Type u_1} [QuasiBorelSpace A] (f : A → ENNReal) (φ : ℝ →𝒒 A) (μ : MeasureTheory.ProbabilityMeasure ℝ) : lintegral f { eval := φ, base := μ } = ∫⁻ (x : ℝ), f (φ x) ∂↑μ

Alias of QuasiBorelSpace.PreProbabilityMeasure.lintegral.eq_1.

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.measureOf {A : Type u_1} [QuasiBorelSpace A] : PreProbabilityMeasure A → Set A → ENNReal

TODO

Equations

• { eval := φ, base := μ }.measureOf x✝ = ↑(μ {x : ℝ | φ x ∈ x✝})

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.measureOf_mk {A : Type u_1} [QuasiBorelSpace A] (x✝ : Set A) (φ : ℝ →𝒒 A) (μ : MeasureTheory.ProbabilityMeasure ℝ) : { eval := φ, base := μ }.measureOf x✝ = ↑(μ {x : ℝ | φ x ∈ x✝})

Alias of QuasiBorelSpace.PreProbabilityMeasure.measureOf.eq_1.

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_eq_measureOf {A : Type u_1} [QuasiBorelSpace A] (μ : PreProbabilityMeasure A) (s : Set A) (hp : IsHom fun (x : A) => x ∈ s) : lintegral (s.indicator 1) μ = μ.measureOf s

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.mk' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] (eval : A →𝒒 B) (base : MeasureTheory.ProbabilityMeasure A) : PreProbabilityMeasure B

A PreProbabilityMeasure can be constructed from any ProbabilityMeasure on a standard borel space.

Equations

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

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_mk' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] {k : B → ENNReal} (hk : IsHom k) (φ : A →𝒒 B) (μ : MeasureTheory.ProbabilityMeasure A) : lintegral k (mk' φ μ) = ∫⁻ (x : A), k (φ x) ∂↑μ

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

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

@[instance_reducible]

instance QuasiBorelSpace.PreProbabilityMeasure.setoid (A : Type u_5) [QuasiBorelSpace A] : Setoid (PreProbabilityMeasure A)

Equations

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

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

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

@[simp]

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

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_mono {A : Type u_1} [QuasiBorelSpace A] {f g : A → ENNReal} (h : f ≤ g) (μ : PreProbabilityMeasure A) : lintegral f μ ≤ lintegral g μ

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

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

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

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_lintegral_swap {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {μ : PreProbabilityMeasure A} {ν : PreProbabilityMeasure B} ⦃f : A → B → ENNReal⦄ (hf : IsHom (Function.uncurry f)) : lintegral (fun (x : A) => lintegral (f x) ν) μ = lintegral (fun (x : B) => lintegral (fun (x_1 : A) => f x_1 x) μ) ν

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.measureOf_empty {B : Type u_2} [QuasiBorelSpace B] (μ : PreProbabilityMeasure B) : μ.measureOf ∅ = 0

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.measureOf_mono {B : Type u_2} [QuasiBorelSpace B] (μ : PreProbabilityMeasure B) : Monotone μ.measureOf

theorem QuasiBorelSpace.PreProbabilityMeasure.measureOf_iUnion_le {A : Type u_1} [QuasiBorelSpace A] {ι : Type u_5} [Countable ι] (μ : PreProbabilityMeasure A) (s : ι → Set A) : μ.measureOf (⋃ (i : ι), s i) ≤ ∑' (i : ι), μ.measureOf (s i)

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.setoid_r {A : Type u_1} [QuasiBorelSpace A] (μ₁ μ₂ : PreProbabilityMeasure A) : (setoid A) μ₁ μ₂ ↔ μ₁ ≈ μ₂

theorem QuasiBorelSpace.PreProbabilityMeasure.equiv_def {A : Type u_1} [QuasiBorelSpace A] (μ₁ μ₂ : PreProbabilityMeasure A) : μ₁ ≈ μ₂ ↔ ∀ {f : A → ENNReal}, IsHom f → lintegral f μ₁ = lintegral f μ₂

theorem QuasiBorelSpace.PreProbabilityMeasure.equiv_def' {A : Type u_1} [QuasiBorelSpace A] (μ₁ μ₂ : PreProbabilityMeasure A) : μ₁ ≈ μ₂ ↔ ∀ {p : Set A}, (IsHom fun (x : A) => x ∈ p) → μ₁.measureOf p = μ₂.measureOf p

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

structure QuasiBorelSpace.PreProbabilityMeasure.Var (A : Type u_5) [QuasiBorelSpace A] : Type u_5

The type of variables for probability measures.

• eval : ℝ →𝒒 A

  The random variable associated with each probability measure.

• base : ℝ → MeasureTheory.ProbabilityMeasure ℝ

  The family of base ProbabilityMeasures.

• measurable_base : Measurable self.base

  The family of base measures is measurable.

def QuasiBorelSpace.PreProbabilityMeasure.Var.apply {A : Type u_1} [QuasiBorelSpace A] : Var A → ℝ → PreProbabilityMeasure A

Evaluates a Var.

Equations

• { eval := φ, base := μ, measurable_base := measurable_base }.apply x✝ = { eval := φ, base := μ x✝ }

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.measureOf_mk {A : Type u_1} [QuasiBorelSpace A] (x✝ : ℝ) (φ : ℝ →𝒒 A) (μ : ℝ → MeasureTheory.ProbabilityMeasure ℝ) (measurable_base : Measurable μ) : { eval := φ, base := μ, measurable_base := measurable_base }.apply x✝ = { eval := φ, base := μ x✝ }

Alias of QuasiBorelSpace.PreProbabilityMeasure.Var.apply.eq_1.

@[instance_reducible]

instance QuasiBorelSpace.PreProbabilityMeasure.Var.instCoeFunForallReal {A : Type u_1} [QuasiBorelSpace A] : CoeFun (Var A) fun (x : Var A) => ℝ → PreProbabilityMeasure A

Equations

• QuasiBorelSpace.PreProbabilityMeasure.Var.instCoeFunForallReal = { coe := QuasiBorelSpace.PreProbabilityMeasure.Var.apply }

def QuasiBorelSpace.PreProbabilityMeasure.Var.const {A : Type u_1} [QuasiBorelSpace A] (μ : PreProbabilityMeasure A) : Var A

The constant variable.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.Var.const μ = { eval := μ.eval, base := fun (x : ℝ) => μ.base, measurable_base := ⋯ }

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.apply_const {A : Type u_1} [QuasiBorelSpace A] (μ : PreProbabilityMeasure A) (r : ℝ) : (const μ).apply r = μ

def QuasiBorelSpace.PreProbabilityMeasure.Var.comp {A : Type u_1} [QuasiBorelSpace A] {f : ℝ → ℝ} (hf : Measurable f) (φ : Var A) : Var A

Precomposition of variables by measurable functions.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.Var.comp hf φ = { eval := φ.eval, base := fun (r : ℝ) => φ.base (f r), measurable_base := ⋯ }

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.apply_comp {A : Type u_1} [QuasiBorelSpace A] {f : ℝ → ℝ} (hf : Measurable f) (φ : Var A) (r : ℝ) : (comp hf φ).apply r = φ.apply (f r)

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.Var.cases {A : Type u_1} [QuasiBorelSpace A] {ix : ℝ → ℕ} (hix : Measurable ix) (φ : ℕ → Var A) : Var A

Gluing of a countable number of variables.

Equations

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

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.apply_cases {A : Type u_1} [QuasiBorelSpace A] {ix : ℝ → ℕ} (hix : Measurable ix) (φ : ℕ → Var A) (r : ℝ) : (cases hix φ).apply r ≈ (φ (ix r)).apply r

@[instance_reducible]

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

Equations

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

theorem QuasiBorelSpace.PreProbabilityMeasure.isHom_def {A : Type u_1} [QuasiBorelSpace A] (φ : ℝ → PreProbabilityMeasure A) : IsHom φ ↔ ∃ (ψ : Var A), ∀ (r : ℝ), φ r ≈ ψ.apply r

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.isHom_apply {A : Type u_1} [QuasiBorelSpace A] (φ : Var A) : IsHom φ.apply

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.subeval {A : Type u_1} [QuasiBorelSpace A] (φ : ℝ → PreProbabilityMeasure A) : ℝ →𝒒 A

The variable associated with a PreProbabilityMeasure variable.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.subeval φ = if hφ : QuasiBorelSpace.IsHom φ then (Classical.choose ⋯).eval else { toFun := fun (x : ℝ) => Classical.choice ⋯, property := ⋯ }

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.subbase {A : Type u_1} [QuasiBorelSpace A] (φ : ℝ → PreProbabilityMeasure A) : ℝ → MeasureTheory.ProbabilityMeasure ℝ

The measure associated with a PreProbabilityMeasure variable.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.subbase φ = if hφ : QuasiBorelSpace.IsHom φ then (Classical.choose ⋯).base else fun (x : ℝ) => default

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.measurable_subbase {A : Type u_1} [QuasiBorelSpace A] (φ : ℝ → PreProbabilityMeasure A) : Measurable (subbase φ)

theorem QuasiBorelSpace.PreProbabilityMeasure.sub_eq {A : Type u_1} [QuasiBorelSpace A] {φ : ℝ → PreProbabilityMeasure A} (hφ : IsHom φ) (r : ℝ) : φ r ≈ { eval := subeval φ, base := subbase φ r }

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

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_congr {A : Type u_1} [QuasiBorelSpace A] {k : A → ENNReal} (hk : IsHom k) {μ₁ μ₂ : PreProbabilityMeasure A} (hμ : μ₁ ≈ μ₂) : lintegral k μ₁ = lintegral k μ₂

theorem QuasiBorelSpace.PreProbabilityMeasure.measureOf_congr {A : Type u_1} [QuasiBorelSpace A] {p : Set A} (hk : IsHom fun (x : A) => x ∈ p) {μ₁ μ₂ : PreProbabilityMeasure A} (hμ : μ₁ ≈ μ₂) : μ₁.measureOf p = μ₂.measureOf p

theorem QuasiBorelSpace.PreProbabilityMeasure.isHom_congr {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {f g : A → PreProbabilityMeasure B} (h : ∀ (x : A), f x ≈ g x) : IsHom f ↔ IsHom g

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

The unit operation, a.k.a. the dirac measure.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.unit x = { eval := { toFun := fun (x_1 : ℝ) => x, property := ⋯ }, base := default }

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.lintegral_unit {A : Type u_1} [QuasiBorelSpace A] (f : A → ENNReal) (x : A) : lintegral f (unit x) = f x

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.Var.unit {A : Type u_1} [QuasiBorelSpace A] {φ : ℝ → A} (hφ : IsHom φ) : Var A

The dirac measure, lifted to variables.

Equations

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

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.apply_unit {A : Type u_1} [QuasiBorelSpace A] {φ : ℝ → A} (hφ : IsHom φ) (r : ℝ) : (unit hφ).apply r ≈ PreProbabilityMeasure.unit (φ r)

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

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

The monadic bind operation for probability measures.

Equations

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

@[simp]

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

theorem QuasiBorelSpace.PreProbabilityMeasure.bind_congr {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {f : A → PreProbabilityMeasure B} (hf : IsHom f) {g : A → PreProbabilityMeasure B} (hg : IsHom g) (h₁ : ∀ (x : A), f x ≈ g x) {μ ν : PreProbabilityMeasure A} (h₂ : μ ≈ ν) : bind f μ ≈ bind g ν

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.Var.bind {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] (f : A → PreProbabilityMeasure B) (φ : Var A) : Var B

The monadic bind, lifted to variables.

Equations

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

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.apply_bind {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {f : A → PreProbabilityMeasure B} (hf : IsHom f) (φ : Var A) (r : ℝ) : (bind f φ).apply r ≈ PreProbabilityMeasure.bind f (φ.apply r)

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

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

The functorial strength operation.

Equations

• QuasiBorelSpace.PreProbabilityMeasure.str x μ = { eval := { toFun := fun (r : ℝ) => (x, μ.eval r), property := ⋯ }, base := μ.base }

@[simp]

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

theorem QuasiBorelSpace.PreProbabilityMeasure.str_congr {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] (x : A) {μ₁ μ₂ : PreProbabilityMeasure B} (hμ : μ₁ ≈ μ₂) : str x μ₁ ≈ str x μ₂

noncomputable def QuasiBorelSpace.PreProbabilityMeasure.Var.str {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {φ : ℝ → A} (hφ : IsHom φ) (ψ : Var B) : Var (A × B)

The functorial strength operation, lifted to variables.

Equations

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

theorem QuasiBorelSpace.PreProbabilityMeasure.Var.apply_str {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {φ : ℝ → A} (hφ : IsHom φ) (ψ : Var B) (r : ℝ) : (str hφ ψ).apply r ≈ PreProbabilityMeasure.str (φ r) (ψ.apply r)

@[simp]

theorem QuasiBorelSpace.PreProbabilityMeasure.isHom_str {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom fun (x : A × PreProbabilityMeasure B) => str x.1 x.2

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

The Bernoulli measure.

Equations

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

@[simp]

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