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} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} : (μ.bind ⇑κ).bind ⇑η = μ.bind ⇑(η.comp κ)

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

This lemma allows to rewrite the composition 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} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [Countable α] [MeasurableSingletonClass α] : μ.bind ⇑κ = sum fun (ω : α) => μ {ω} • κ ω

@[simp]

theorem MeasureTheory.Measure.snd_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α) [SFinite μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : (μ.compProd κ).snd = μ.bind ⇑κ

theorem MeasureTheory.Measure.comp_congr {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ η : ProbabilityTheory.Kernel α β} (h : ∀ᵐ (a : α) ∂μ, κ a = η a) : μ.bind ⇑κ = μ.bind ⇑η

theorem MeasureTheory.Measure.ae_ae_of_ae_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {p : β → Prop} (h : ∀ᵐ (ω : β) ∂μ.bind ⇑κ, p ω) : ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω

theorem MeasureTheory.Measure.ae_comp_of_ae_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {p : β → Prop} (hp : MeasurableSet {z : β | p z}) (h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z) : ∀ᵐ (z : β) ∂μ.bind ⇑κ, p z

theorem MeasureTheory.Measure.ae_comp_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {p : β → Prop} (hp : MeasurableSet {z : β | p z}) : (∀ᵐ (z : β) ∂μ.bind ⇑κ, p z) ↔ ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z

instance MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] : SFinite (μ.bind ⇑κ)

instance MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] : IsFiniteMeasure (μ.bind ⇑κ)

instance MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ] : IsProbabilityMeasure (μ.bind ⇑κ)

instance MeasureTheory.Measure.instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.IsZeroOrMarkovKernel κ] : IsZeroOrProbabilityMeasure (μ.bind ⇑κ)

@[simp]

theorem ProbabilityTheory.Kernel.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel β γ) (μ : MeasureTheory.Measure β) : κ.comp (const α μ) = const α (μ.bind ⇑κ)

theorem MeasureTheory.Measure.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (μ : Measure α) (κ : ProbabilityTheory.Kernel α β) {f : β → γ} (hf : Measurable f) : map f (μ.bind ⇑κ) = μ.bind ⇑(κ.map f)

@[simp]

theorem MeasureTheory.Measure.discard_comp {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) : μ.bind ⇑(ProbabilityTheory.Kernel.discard α) = μ Set.univ • dirac ()

theorem MeasureTheory.Measure.copy_comp_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) : (map f μ).bind ⇑(ProbabilityTheory.Kernel.copy β) = map (Function.prod f f) μ

theorem MeasureTheory.Measure.compProd_eq_comp_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α) [SFinite μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : μ.compProd κ = μ.bind ⇑(ProbabilityTheory.Kernel.id.prod κ)

theorem MeasureTheory.Measure.compProd_id_eq_copy_comp {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SFinite μ] : μ.compProd ProbabilityTheory.Kernel.id = μ.bind ⇑(ProbabilityTheory.Kernel.copy α)

theorem MeasureTheory.Measure.comp_compProd_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : 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} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} [SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] : (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.prodMkLeft α η) = (μ.bind ⇑κ).bind ⇑η

theorem MeasureTheory.Measure.compProd_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ] {f : α → β} (hf : Measurable f) : μ.compProd (ProbabilityTheory.Kernel.deterministic f hf) = map (fun (a : α) => (a, f a)) μ

@[simp]

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

theorem MeasureTheory.Measure.add_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ η : ProbabilityTheory.Kernel α β} : μ.bind ⇑(κ + η) = μ.bind ⇑κ + μ.bind ⇑η

@[simp]

theorem MeasureTheory.Measure.add_comp' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : 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} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} (a : ENNReal) : (a • μ).bind ⇑κ = a • μ.bind ⇑κ

theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_right {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ ν : Measure α} (hμν : μ.AbsolutelyContinuous ν) (κ : ProbabilityTheory.Kernel α γ) : (μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑κ)

theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β} (μ : Measure α) (hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) : (μ.bind ⇑κ).AbsolutelyContinuous (μ.bind ⇑η)

theorem MeasureTheory.Measure.AbsolutelyContinuous.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : Measure α} {κ η : ProbabilityTheory.Kernel α β} (hμν : μ.AbsolutelyContinuous ν) (hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) : (μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑η)

theorem MeasureTheory.Measure.absolutelyContinuous_comp_of_countable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [Countable α] [MeasurableSingletonClass α] : ∀ᵐ (ω : α) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)

@[simp]

theorem ProbabilityTheory.Kernel.comp_boolKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (μ ν : MeasureTheory.Measure α) : κ.comp (boolKernel μ ν) = boolKernel (μ.bind ⇑κ) (ν.bind ⇑κ)

theorem ProbabilityTheory.boolKernel_comp_measure {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (π : MeasureTheory.Measure Bool) : π.bind ⇑(Kernel.boolKernel μ ν) = π {true} • ν + π {false} • μ

theorem ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left {α : Type u_1} {mα : MeasurableSpace α} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure α) (hπ : π {false} ≠ 0) : μ.AbsolutelyContinuous (π.bind ⇑(Kernel.boolKernel μ ν))

theorem ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right {α : Type u_1} {mα : MeasurableSpace α} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure α) (hπ : π {true} ≠ 0) : ν.AbsolutelyContinuous (π.bind ⇑(Kernel.boolKernel μ ν))