compProd_null — Mathlib

English

Under measurability assumptions, the lintegral against κ ⊗ η equals the iterated lintegrals against η and κ.

Русский

При допустимых условия измеримости линегральный интеграл против κ ⊗ η равен повторному интегралу над η и κ.

LaTeX

$$$$ \int f \; d(κ \otimes_k η) a = \int κ(a)(db) \int η(a,b)(dc) f(b,c). $$$$

Lean4

theorem compProd_null (a : α) (hs : MeasurableSet s) :
    (κ ⊗ₖ η) a s = 0 ↔ (fun b => η (a, b) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0 :=
  by
  rw [Kernel.compProd_apply hs, lintegral_eq_zero_iff]
  exact Kernel.measurable_kernel_prodMk_left' hs a

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