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 β γ}
:
theorem
MeasureTheory.Measure.comp_eq_comp_const_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : 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 ∘ₘ.
@[simp]
theorem
MeasureTheory.Measure.snd_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
[SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
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 ω)
:
instance
MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
:
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 ⇑κ)
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)
:
theorem
MeasureTheory.Measure.compProd_eq_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
[SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
MeasureTheory.Measure.compProd_id_eq_copy_comp
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[SFinite μ]
:
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 η]
:
theorem
MeasureTheory.Measure.integrable_compProd_snd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
{f : β → E}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
(hf : AEStronglyMeasurable f (μ.bind ⇑κ))
:
theorem
MeasureTheory.Measure.ae_integrable_of_integrable_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
{f : β → E}
(h_int : Integrable f (μ.bind ⇑κ))
:
∀ᵐ (x : α) ∂μ, Integrable f (κ x)
theorem
MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
{f : β → E}
(h_int : Integrable f (μ.bind ⇑κ))
:
@[simp]
theorem
MeasureTheory.Measure.comp_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ : ProbabilityTheory.Kernel α β}
:
theorem
MeasureTheory.Measure.add_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
:
@[simp]
theorem
MeasureTheory.Measure.add_comp'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
:
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)
:
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 ⇑η)