compProd_eq_zero_iff — Mathlib

English

Equivalence between κ ⊗ₖ η = 0 and the almost-everywhere zero condition on η given κ.

Русский

Эквивалентность между κ ⊗ₖ η = 0 и почти всюду нулем η с учетом κ.

LaTeX

$$$$ κ ⊗ₖ η = 0 \;\; \Leftrightarrow \;\; \forall a, ∀ᵐ b ∂(κ a), η(a,b) = 0. $$$$

Lean4

theorem compProd_eq_zero_iff {κ : Kernel α β} {η : Kernel (α × β) γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    κ ⊗ₖ η = 0 ↔ ∀ a, ∀ᵐ b ∂(κ a), η (a, b) = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simp_rw [← Measure.measure_univ_eq_zero]
    refine fun a ↦ (lintegral_eq_zero_iff ?_).mp ?_
    · exact (η.measurable_coe .univ).comp measurable_prodMk_left
    · rw [← setLIntegral_univ, ← Kernel.compProd_apply_prod .univ .univ, h]
      simp
  · rw [← Kernel.compProd_zero_right κ]
    exact Kernel.compProd_congr h

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