# Lemmas about the composition of a measure and a kernel #

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

source
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 κ)
source
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 `∘ₘ`.

source
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 (ω : α) => μ {ω} • κ ω
source
@[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 ⇑κ
source
theorem MeasureTheory.Measure.comp_congr {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ η : ProbabilityTheory.Kernel α β} (h : ∀ᵐ (a : α) ∂μ, κ a = η a) :
μ.bind ⇑κ = μ.bind ⇑η
source
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 ω
source
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
source
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
source
instance MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] :
SFinite (μ.bind ⇑κ)
source
instance MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] :
IsFiniteMeasure (μ.bind ⇑κ)
source
instance MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ] :
IsProbabilityMeasure (μ.bind ⇑κ)
source
instance MeasureTheory.Measure.instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.IsZeroOrMarkovKernel κ] :
IsZeroOrProbabilityMeasure (μ.bind ⇑κ)
source
@[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 ⇑κ)
source
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)
source
@[simp]
theorem MeasureTheory.Measure.discard_comp {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) :
μ.bind ⇑(ProbabilityTheory.Kernel.discard α) = μ Set.univ • dirac ()
source
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 (fun (a : α) => (f a, f a)) μ
source
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 κ)
source
theorem MeasureTheory.Measure.compProd_id_eq_copy_comp {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SFinite μ] :
μ.compProd ProbabilityTheory.Kernel.id = μ.bind ⇑(ProbabilityTheory.Kernel.copy α)
source
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
source
@[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 ⇑η
source
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)) μ
source
@[simp]
theorem MeasureTheory.Measure.comp_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : Measure α} {κ : ProbabilityTheory.Kernel α β} :
(μ + ν).bind ⇑κ = μ.bind ⇑κ + ν.bind ⇑κ
source
theorem MeasureTheory.Measure.add_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ η : ProbabilityTheory.Kernel α β} :
μ.bind ⇑(κ + η) = μ.bind ⇑κ + μ.bind ⇑η
source
@[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.

source
@[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 ⇑κ
source
theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_right {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ ν : Measure α} (hμν : μ.AbsolutelyContinuous ν) (κ : ProbabilityTheory.Kernel α γ) :
(μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑κ)
source
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 ⇑η)
source
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 ⇑η)
source
theorem MeasureTheory.Measure.absolutelyContinuous_comp_of_countable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [Countable α] [MeasurableSingletonClass α] :
∀ᵐ (ω : α) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)
source
@[simp]
theorem ProbabilityTheory.Kernel.comp_boolKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (μ ν : MeasureTheory.Measure α) :
κ.comp (boolKernel μ ν) = boolKernel (μ.bind ⇑κ) (ν.bind ⇑κ)
source
theorem ProbabilityTheory.boolKernel_comp_measure {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (π : MeasureTheory.Measure Bool) :
π.bind ⇑(Kernel.boolKernel μ ν) = π {true} • ν + π {false} • μ
source
theorem ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left {α : Type u_1} {mα : MeasurableSpace α} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure α) (hπ : π {false} ≠ 0) :
μ.AbsolutelyContinuous (π.bind ⇑(Kernel.boolKernel μ ν))
source
theorem ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right {α : Type u_1} {mα : MeasurableSpace α} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure α) (hπ : π {true} ≠ 0) :
ν.AbsolutelyContinuous (π.bind ⇑(Kernel.boolKernel μ ν))