mutuallySingular_compProd_iff — Mathlib

English

A simplified version of the prior equivalence using prodAssoc.

Русский

Упрощённая версия эквивалентности через prodAssoc.

LaTeX

$$$((μ ⊗ₘ κ).MutuallySingular (ν ⊗ₘ κ)) \\iff (μ ⟂ ν)$$$

Lean4

theorem mutuallySingular_compProd_iff [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η :=
  by
  conv_lhs => rw [ν.haveLebesgueDecomposition_add μ]
  rw [compProd_add_left, MutuallySingular.add_right_iff]
  simp only [(mutuallySingular_singularPart ν μ).symm.compProd_of_left κ η, true_and]
  refine ⟨fun h ↦ h.mono_ac .rfl ?_, fun h ↦ h.mono_ac .rfl ?_⟩
  · exact (absolutelyContinuous_withDensity_rnDeriv hμν).compProd_left _
  · exact (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).compProd_left _

Похожие утверждения