kernel_of_compProd — Mathlib

English

If μ ⊗ₘ κ ≪ ν ⊗ₘ η with μ finite, then κ a ≪ η a for μ-almost every a.

Русский

Если μ ⊗ₘ κ эквивалентно absolutely continuous к ν ⊗ₘ η, то κ(a) ≪ η(a) для μ-почти всех a.

LaTeX

$$$(μ ⊗_m κ) \\ll (ν ⊗_m η) \\quad\\Rightarrow\\quad \\forall^{\\text{ae}} a\\partial μ,\\ κ(a) \\ll η(a).$$$

Lean4

theorem kernel_of_compProd [SFinite μ] (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) : ∀ᵐ a ∂μ, κ a ≪ η a :=
  by
  suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by
    filter_upwards [this] with a ha
    rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha
  rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h
  have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η :=
    MutuallySingular.compProd_of_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _)
  refine compProd_eq_zero_iff.mp ?_
  exact eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this

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