Condition for two kernels to be equal almost everywhere #
We prove that two finite kernels κ, η : Kernel α β are μ-a.e. equal for a finite measure μ iff
the composition-products μ ⊗ₘ κ and μ ⊗ₘ η are equal.
The result requires α to be countable or β to be a countably generated measurable space.
Main statements #
compProd_withDensity:μ ⊗ₘ (κ.withDensity f) = (μ ⊗ₘ κ).withDensity (fun p ↦ f p.1 p.2)compProd_eq_iff:μ ⊗ₘ κ = μ ⊗ₘ η ↔ κ =ᵐ[μ] η
theorem
MeasureTheory.Measure.compProd_withDensity
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{f : α → β → ENNReal}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)]
(hf : Measurable (Function.uncurry f))
:
A composition-product of a measure with a kernel defined with withDensity is equal to the
withDensity of the composition-product.
theorem
ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ η : Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
[IsFiniteKernel η]
(h : μ.compProd κ = μ.compProd η)
:
theorem
ProbabilityTheory.Kernel.compProd_eq_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ η : Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
[IsFiniteKernel η]
:
Two finite kernels κ and η are μ-a.e. equal iff the composition-products μ ⊗ₘ κ
and μ ⊗ₘ η are equal.