Proper kernels

This file defines properness of measure kernels.

For two σ-algebras 𝓑 ≤ 𝓧, a 𝓑, 𝓧-kernel π : X → Measure X is proper if ∫ x, g x * f x ∂(π x₀) = g x₀ * ∫ x, f x ∂(π x₀) for all x₀ : X, 𝓧-measurable function f and 𝓑-measurable function g.

By the standard machine, this is equivalent to having that, for all B ∈ 𝓑, π restricted to B is the same as π times the indicator of B.

This should be thought of as the condition under which one can meaningfully restrict a kernel to an event.

TODO

Prove the integral versions of the lintegral lemmas below

structure ProbabilityTheory.Kernel.IsProper {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} (π : Kernel X X) : Prop

For two σ-algebras 𝓑 ≤ 𝓧 on a space X, a 𝓑, 𝓧-kernel π : X → Measure X is proper if ∫ x, g x * f x ∂(π x₀) = g x₀ * ∫ x, f x ∂(π x₀) for all x₀ : X, 𝓧-measurable function f and 𝓑-measurable function g.

By the standard machine, this is equivalent to having that, for all B ∈ 𝓑, π restricted to B is the same as π times the indicator of B.

To avoid assuming 𝓑 ≤ 𝓧 in the definition, we replace 𝓑 by 𝓑 ⊓ 𝓧 in the restriction.

• restrict_eq_indicator_smul' ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) : (π.restrict ⋯) x = B.indicator (fun (x : X) => 1) x • π x

theorem ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧) : π.IsProper ↔ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun (x : X) => 1) x • π x

theorem ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧) : π.IsProper ↔ ∀ ⦃A : Set X⦄, MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

theorem ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧) : π.IsProper → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun (x : X) => 1) x • π x

Alias of the forward direction of ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul.

theorem ProbabilityTheory.Kernel.IsProper.of_restrict_eq_indicator_smul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧) : (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun (x : X) => 1) x • π x) → π.IsProper

Alias of the reverse direction of ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul.

theorem ProbabilityTheory.Kernel.IsProper.of_inter_eq_indicator_mul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧) : (∀ ⦃A : Set X⦄, MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A) → π.IsProper

Alias of the reverse direction of ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul.

theorem ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧) : π.IsProper → ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (_hB : MeasurableSet B) (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Alias of the forward direction of ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul.

theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_comp {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {A B : Set X} (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) {μ : MeasureTheory.Measure X} (hA : MeasurableSet A) (hB : MeasurableSet B) : ∫⁻ (a : X) in B, (π a) A ∂μ = (μ.bind ⇑π) (A ∩ B)

theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_indicator_mul_lintegral {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {B : Set X} {f : X → ENNReal} (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable f) (hB : MeasurableSet B) (x₀ : X) : ∫⁻ (x : X) in B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀

theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {A B : Set X} {f : X → ENNReal} (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable f) (hA : MeasurableSet A) (hB : MeasurableSet B) (x₀ : X) : ∫⁻ (x : X) in A ∩ B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X) in A, f x ∂π x₀

theorem ProbabilityTheory.Kernel.IsProper.lintegral_mul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {f g : X → ENNReal} (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable f) (hg : Measurable g) (x₀ : X) : ∫⁻ (x : X), g x * f x ∂π x₀ = g x₀ * ∫⁻ (x : X), f x ∂π x₀