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 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 α]
:
@[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.comp_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
(h : ∀ᵐ (a : α) ∂μ, κ a = η a)
:
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 ω)
:
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)
:
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})
:
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 ⇑κ)
@[simp]
theorem
ProbabilityTheory.Kernel.comp_const
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel β γ)
(μ : MeasureTheory.Measure β)
:
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)
:
@[simp]
theorem
MeasureTheory.Measure.discard_comp
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
:
theorem
MeasureTheory.Measure.copy_comp_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable 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 η]
:
@[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 κ]
:
theorem
MeasureTheory.Measure.compProd_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
[SFinite μ]
{f : α → β}
(hf : Measurable f)
:
@[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 ⇑η)
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 α)
:
theorem
ProbabilityTheory.boolKernel_comp_measure
{α : Type u_1}
{mα : MeasurableSpace α}
(μ ν : MeasureTheory.Measure α)
(π : MeasureTheory.Measure Bool)
:
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 μ ν))