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.