English
Under finiteness and nonzero assumptions, μ ⊗ κ ≪ ν ⊗ η iff μ ≪ ν and μ ⊗ κ ≪ μ ⊗ η.
Русский
При конечности и ненулевых предпосылках μ ⊗ κ ≪ ν ⊗ η тогда и только тогда μ ≪ ν и μ ⊗ κ ≪ μ ⊗ η.
LaTeX
$$$[\\text{SFinite}(\\mu)][\\text{SigmaFinite}(\\nu)] [IsSFiniteKernel κ][IsSFiniteKernel η] [∀ x, NeZero(κ(x))] : (μ ⊗ₘ κ) ≪ (ν ⊗ₘ η)\\iff (μ ≪ ν ∧ (μ ⊗ₘ κ) ≪ (μ ⊗ₘ η))$$
Lean4
theorem mutuallySingular_compProd_iff [SigmaFinite μ] [SigmaFinite ν] :
μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ ξ, SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η :=
by
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
rw [compProd_add_left, MutuallySingular.add_left_iff]
simp only [(mutuallySingular_singularPart μ ν).compProd_of_left κ η, true_and]
rw [(withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).mutuallySingular_compProd_iff]
refine ⟨fun h ξ hξ hξμ hξν ↦ ?_, fun h ↦ ?_⟩
· exact h.mono_ac ((hξμ.withDensity_rnDeriv hξν).compProd_left _) ((hξμ.withDensity_rnDeriv hξν).compProd_left _)
· refine h _ ?_ ?_ ?_
· infer_instance
· exact absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _)
· exact withDensity_absolutelyContinuous ν (μ.rnDeriv ν)
