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

source
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)) :
μ.compProd (κ.withDensity f) = (μ.compProd κ).withDensity fun (p : α × β) => f p.1 p.2

A composition-product of a measure with a kernel defined with `withDensity` is equal to the `withDensity` of the composition-product.

source
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 η) :
⇑κ =ᵐ[μ] ⇑η
source
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 η] :
μ.compProd κ = μ.compProd η ↔ ⇑κ =ᵐ[μ] ⇑η

Two finite kernels `κ` and `η` are `μ`-a.e. equal iff the composition-products `μ ⊗ₘ κ` and `μ ⊗ₘ η` are equal.