Documentation

Mathlib.Probability.Kernel.Composition.MeasureComp

Lemmas about the composition of a measure and a kernel #

Basic lemmas about the composition κ ∘ₘ μ of a kernel κ and a measure μ.

theorem MeasureTheory.Measure.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} :
(μ.bind κ).bind η = μ.bind (η.comp κ)
theorem MeasureTheory.Measure.comp_eq_comp_const_apply {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} :

This lemma allows to rewrite the compostion of a measure and a kernel as the composition of two kernels, which allows to transfer properties of ∘ₖ to ∘ₘ.

theorem MeasureTheory.Measure.comp_eq_sum_of_countable {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [Countable α] [MeasurableSingletonClass α] :
μ.bind κ = sum fun (ω : α) => μ {ω} κ ω
@[simp]
theorem MeasureTheory.Measure.snd_compProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (μ : Measure α) [SFinite μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] :
(μ.compProd κ).snd = μ.bind κ
theorem MeasureTheory.Measure.ae_ae_of_ae_comp {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {p : βProp} (h : ∀ᵐ (ω : β) μ.bind κ, p ω) :
∀ᵐ (ω' : α) μ, ∀ᵐ (ω : β) κ ω', p ω
theorem MeasureTheory.Measure.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (μ : Measure α) (κ : ProbabilityTheory.Kernel α β) {f : βγ} (hf : Measurable f) :
map f (μ.bind κ) = μ.bind (κ.map f)
theorem MeasureTheory.Measure.comp_compProd_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel (α × β) γ} [SFinite μ] [ProbabilityTheory.IsSFiniteKernel η] :
(μ.compProd κ).bind η = (μ.bind (κ.compProd η)).snd
@[simp]
theorem MeasureTheory.Measure.prodMkLeft_comp_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} [SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] :
(μ.compProd κ).bind (ProbabilityTheory.Kernel.prodMkLeft α η) = (μ.bind κ).bind η
@[simp]
theorem MeasureTheory.Measure.comp_add {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ ν : Measure α} {κ : ProbabilityTheory.Kernel α β} :
(μ + ν).bind κ = μ.bind κ + ν.bind κ
theorem MeasureTheory.Measure.add_comp {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ : Measure α} {κ η : ProbabilityTheory.Kernel α β} :
μ.bind ⇑(κ + η) = μ.bind κ + μ.bind η
@[simp]
theorem MeasureTheory.Measure.add_comp' {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ : Measure α} {κ η : ProbabilityTheory.Kernel α β} :
μ.bind (κ + η) = μ.bind κ + μ.bind η

Same as add_comp except that it uses ⇑κ + ⇑η instead of ⇑(κ + η) in order to have a simp-normal form on the left of the equality.

@[simp]
theorem MeasureTheory.Measure.comp_smul {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} (a : ENNReal) :
(a μ).bind κ = a μ.bind κ
theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_right {α : Type u_1} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace γ} {μ ν : Measure α} (hμν : μ.AbsolutelyContinuous ν) (κ : ProbabilityTheory.Kernel α γ) :
(μ.bind κ).AbsolutelyContinuous (ν.bind κ)
theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_left {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β} (μ : Measure α) (hκη : ∀ᵐ (a : α) μ, (κ a).AbsolutelyContinuous (η a)) :
(μ.bind κ).AbsolutelyContinuous (μ.bind η)
theorem MeasureTheory.Measure.AbsolutelyContinuous.comp {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {μ ν : Measure α} {κ η : ProbabilityTheory.Kernel α β} (hμν : μ.AbsolutelyContinuous ν) (hκη : ∀ᵐ (a : α) μ, (κ a).AbsolutelyContinuous (η a)) :
(μ.bind κ).AbsolutelyContinuous (ν.bind η)