compProd_eq_zero_iff — Mathlib

English

For SFinite μ and IsSFiniteKernel κ, μ ⊗ₘ κ = 0 if and only if κ a = 0 for μ-almost every a.

Русский

Для SFinite μ и IsSFiniteKernel κ верно: μ ⊗ₘ κ = 0 тогда и только тогда, когда κ(a) = 0 почти все a по μ.

LaTeX

$$$[\\mathrm{SFinite}\\; μ] [\\mathrm{IsSFiniteKernel}\\; κ] : μ ⊗_m κ = 0 \\iff (∀^{\\mathrm{ae}} a \\partial μ, κ a = 0)$$$

Lean4

theorem compProd_eq_zero_iff [SFinite μ] [IsSFiniteKernel κ] : μ ⊗ₘ κ = 0 ↔ ∀ᵐ a ∂μ, κ a = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simp_rw [← measure_univ_eq_zero]
    refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_
    rw [← setLIntegral_univ, ← compProd_apply_prod .univ .univ, h]
    simp
  · rw [← compProd_zero_right μ]
    exact compProd_congr h

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