Invariance of measures along a kernel

We say that a measure μ is invariant with respect to a kernel κ if its push-forward along the kernel μ.bind κ is the same measure.

Main definitions

• ProbabilityTheory.kernel.Invariant: invariance of a given measure with respect to a kernel.

Useful lemmas

• ProbabilityTheory.kernel.const_bind_eq_comp_const, and ProbabilityTheory.kernel.comp_const_apply_eq_bind established the relationship between the push-forward measure and the composition of kernels.

Push-forward of measures along a kernel

@[simp]

theorem ProbabilityTheory.kernel.bind_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ↥(ProbabilityTheory.kernel α β)) : MeasureTheory.Measure.bind (μ + ν) ⇑κ = MeasureTheory.Measure.bind μ ⇑κ + MeasureTheory.Measure.bind ν ⇑κ

@[simp]

theorem ProbabilityTheory.kernel.bind_smul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) (μ : MeasureTheory.Measure α) (r : ENNReal) : MeasureTheory.Measure.bind (r • μ) ⇑κ = r • MeasureTheory.Measure.bind μ ⇑κ

theorem ProbabilityTheory.kernel.const_bind_eq_comp_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) (μ : MeasureTheory.Measure α) : ProbabilityTheory.kernel.const α (MeasureTheory.Measure.bind μ ⇑κ) = ProbabilityTheory.kernel.comp κ (ProbabilityTheory.kernel.const α μ)

theorem ProbabilityTheory.kernel.comp_const_apply_eq_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) (μ : MeasureTheory.Measure α) (a : α) : (ProbabilityTheory.kernel.comp κ (ProbabilityTheory.kernel.const α μ)) a = MeasureTheory.Measure.bind μ ⇑κ

Invariant measures of kernels

def ProbabilityTheory.kernel.Invariant {α : Type u_1} {mα : MeasurableSpace α} (κ : ↥(ProbabilityTheory.kernel α α)) (μ : MeasureTheory.Measure α) : Prop

A measure μ is invariant with respect to the kernel κ if the push-forward measure of μ along κ equals μ.

Equations

• ProbabilityTheory.kernel.Invariant κ μ = (MeasureTheory.Measure.bind μ ⇑κ = μ)

theorem ProbabilityTheory.kernel.Invariant.def {α : Type u_1} {mα : MeasurableSpace α} {κ : ↥(ProbabilityTheory.kernel α α)} {μ : MeasureTheory.Measure α} (hκ : ProbabilityTheory.kernel.Invariant κ μ) : MeasureTheory.Measure.bind μ ⇑κ = μ

theorem ProbabilityTheory.kernel.Invariant.comp_const {α : Type u_1} {mα : MeasurableSpace α} {κ : ↥(ProbabilityTheory.kernel α α)} {μ : MeasureTheory.Measure α} (hκ : ProbabilityTheory.kernel.Invariant κ μ) : ProbabilityTheory.kernel.comp κ (ProbabilityTheory.kernel.const α μ) = ProbabilityTheory.kernel.const α μ

theorem ProbabilityTheory.kernel.Invariant.comp {α : Type u_1} {mα : MeasurableSpace α} {κ : ↥(ProbabilityTheory.kernel α α)} {η : ↥(ProbabilityTheory.kernel α α)} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsSFiniteKernel κ] (hκ : ProbabilityTheory.kernel.Invariant κ μ) (hη : ProbabilityTheory.kernel.Invariant η μ) : ProbabilityTheory.kernel.Invariant (ProbabilityTheory.kernel.comp κ η) μ