English
If μ ⊗ κ = μ ⊗ η for finite μ and finite kernels κ, η, then κ =ᵐ[μ] η.
Русский
Если μ ⊗ κ = μ ⊗ η при конечной μ и κ, η, тогда κ эквивалентно η почти по μ.
LaTeX
$$$\\kappa =_{a.e.}^{\\mu} \\eta$ given $\\mu \\otimes \\kappa = \\mu \\otimes \\eta$$$
Lean4
theorem ae_eq_of_compProd_eq [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (h : μ ⊗ₘ κ = μ ⊗ₘ η) :
κ =ᵐ[μ] η :=
by
have h_ac : ∀ᵐ a ∂μ, κ a ≪ η a := (Measure.absolutelyContinuous_of_eq h).kernel_of_compProd
have hκ_eq : ∀ᵐ a ∂μ, κ a = η.withDensity (κ.rnDeriv η) a := by
filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm
suffices ∀ᵐ a ∂μ, ∀ᵐ b ∂(η a), κ.rnDeriv η a b = 1 by
filter_upwards [h_ac, this] with a h_ac h using (rnDeriv_eq_one_iff_eq h_ac).mp h
refine Measure.ae_ae_of_ae_compProd (p := fun x ↦ κ.rnDeriv η x.1 x.2 = 1) ?_
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (by fun_prop) fun s hs _ ↦ ?_
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, one_mul]
calc
∫⁻ x in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η
_ = (μ ⊗ₘ κ) s :=
by
rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]
fun_prop
_ = (μ ⊗ₘ η) s := by rw [h]
