compProd_right — Mathlib

English

If μ is finite and κ is SFinite, and κ ≪ η holds μ-a.e., then μ ⊗ₘ κ ≪ μ ⊗ₘ η.

Русский

Если μ конечна и κ — SFinite, и κ ≪ η почти всюду по μ, то μ ⊗ₘ κ ≪ μ ⊗ₘ η.

LaTeX

$$$[\\text{SFinite}(\\mu)] \\rightarrow [IsSFiniteKernel(\\eta)]\\; (h\\kappa : \\forall a, \\kappa(a) \\ll \\eta(a)) \\Rightarrow (\\mu \\otimes_m \\kappa) \\ll (\\mu \\otimes_m \\eta)$$$

Lean4

theorem compProd_right [SFinite μ] [IsSFiniteKernel η] (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : μ ⊗ₘ κ ≪ μ ⊗ₘ η :=
  by
  by_cases hκ : IsSFiniteKernel κ
  · refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
    rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)] at hs_zero ⊢
    filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero
  · simp [compProd_of_not_isSFiniteKernel _ _ hκ]

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