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 β γ}
:
@[simp]
theorem
MeasureTheory.Measure.snd_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
[SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
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 κ]
:
@[simp]
theorem
MeasureTheory.Measure.comp_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
MeasureTheory.Measure.add_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
@[simp]
theorem
MeasureTheory.Measure.add_comp'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
Same as add_comp except that it uses ⇑κ + ⇑η instead of ⇑(κ + η) in order to have
a simp-normal form on the left of the equality.
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
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SFinite μ]
[SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(hμν : μ.AbsolutelyContinuous ν)
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
(μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑η)
theorem
MeasureTheory.Measure.AbsolutelyContinuous.comp_right
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ ν : Measure α}
[SFinite μ]
[SFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
(κ : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsSFiniteKernel κ]
:
(μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑κ)
theorem
MeasureTheory.Measure.AbsolutelyContinuous.comp_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(μ : Measure α)
[SFinite μ]
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
(μ.bind ⇑κ).AbsolutelyContinuous (μ.bind ⇑η)