setLIntegral_compProd — Mathlib

English

The set-wise version of the composition product allows pulling out integrals over s × t and then integrating fiberwise over a in s and b in t.

Русский

Версия для линограции посетам позволяет вынести интеграцию по s × t и затем по a ∈ s и b ∈ t.

LaTeX

$$$[\\mathrm{SFinite}\\; μ] [IsSFiniteKernel\\ κ] {f : α × β → \\mathbb{R}_{\\ge 0}^{\\infty}} (hf : \\mathrm{Measurable} f) {s : \\mathrm{Set} α} (hs : \\mathrm{MeasurableSet} s) {t : \\mathrm{Set} β} (ht : \\mathrm{MeasurableSet} t) :$$

Lean4

theorem setLIntegral_compProd [SFinite μ] [IsSFiniteKernel κ] {f : α × β → ℝ≥0∞} (hf : Measurable f) {s : Set α}
    (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) :
    ∫⁻ x in s ×ˢ t, f x ∂(μ ⊗ₘ κ) = ∫⁻ a in s, ∫⁻ b in t, f (a, b) ∂(κ a) ∂μ :=
  by
  rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]
  simp

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