compProd_of_compProd — Mathlib

English

If ν ≪ μ and μ ≪ ν (mutually absolutely continuous) then μ ⊗ κ ≪ ν ⊗ η given κ ≪ η.

Русский

Если ν почти всюду меньше μ и μ почти всюду меньше ν, тогда μ ⊗ κ ⪯ ν ⊗ η, если κ ⪯ η.

LaTeX

$$$[SFinite ν] [IsSFiniteKernel η] (hμν: μ ⪯ ν) (hκη: μ ⊗ κ ⊗ η)$ : $μ ⊗ κ ⪯ ν ⊗ η$$$

Lean4

theorem compProd_of_compProd [SFinite ν] [IsSFiniteKernel η] (hμν : μ ≪ ν) (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) : μ ⊗ₘ κ ≪ ν ⊗ₘ η :=
  by
  by_cases hμ : SFinite μ
  swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
  refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
  suffices (μ ⊗ₘ η) s = 0 from hκη this
  rw [measure_eq_zero_iff_ae_notMem, ae_compProd_iff hs.compl] at hs_zero ⊢
  exact hμν.ae_le hs_zero

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