absolutelyContinuous_compProd_of_compProd

English

If μ ⊗ κ ≪ ν ⊗ η, then μ ⊗ κ ≪ μ ⊗ η, under Sigma-finite assumptions and nondegeneracy.

Русский

Если μ ⊗ κ ⪯ ν ⊗ η и условия необходимы, то μ ⊗ κ ⪯ μ ⊗ η.

LaTeX

$$[SigmaFinite μ][SigmaFinite ν](hκη : μ ⊗ κ ≪ ν ⊗ η) : μ ⊗ κ ≪ μ ⊗ η$$

Lean4

theorem absolutelyContinuous_compProd_of_compProd [SigmaFinite μ] [SigmaFinite ν] (hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
    μ ⊗ₘ κ ≪ μ ⊗ₘ η :=
  by
  rw [ν.haveLebesgueDecomposition_add μ, compProd_add_left, add_comm] at hκη
  have h :=
    absolutelyContinuous_of_add_of_mutuallySingular hκη ((mutuallySingular_singularPart _ _).symm.compProd_of_left _ _)
  refine h.trans (AbsolutelyContinuous.compProd_left ?_ _)
  exact withDensity_absolutelyContinuous _ _

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