compProd — Mathlib

English

If μ ⪯ ν and κ a ⪯ η a almost everywhere, then μ ⊗ κ ⪯ ν ⊗ η in the absolutely continuous sense.

Русский

Если μ ⪯ ν и κ a ⪯ η a почти всюду, тогда μ ⊗ κ ⪯ ν ⊗ η по отношению к абсолютной непрерывности.

LaTeX

$$$\\mu \\ll \\nu \\; \\Rightarrow \\; (\\mu \\otimes_m \\kappa) \\ll (\\nu \\otimes_m \\eta)$$$

Lean4

theorem compProd [SFinite ν] [IsSFiniteKernel η] (hμν : μ ≪ ν) (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : μ ⊗ₘ κ ≪ ν ⊗ₘ η :=
  have : SFinite μ := sFinite_of_absolutelyContinuous hμν
  (Measure.AbsolutelyContinuous.compProd_right hκη).trans (hμν.compProd_left _)

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