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_eq_iff:μ ⊗ₘ κ = μ ⊗ₘ η ↔ κ =ᵐ[μ] η
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.