setIntegral_compProd — Mathlib

English

For γ → E with integrable f,g under (η ∘ₖ κ) a, the double integral of (f+g) equals the sum of double integrals of f and g.

Русский

Для функций f,g : γ → E с интегрируемостью, двойной интеграл суммы равен сумме двойных интегралов.

LaTeX

$$$$ \\int x \\int y (f(y) + g(y)) dη_x(y) dκ a = \\int x \\int y f(y) dη_x(y) dκ a + \\int x \\int y g(y) dη_x(y) dκ a $$$$

Lean4

theorem setIntegral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) {f : α × β → E}
    (hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)) : ∫ x in s ×ˢ t, f x ∂(μ ⊗ₘ κ) = ∫ a in s, ∫ b in t, f (a, b) ∂(κ a) ∂μ :=
  by
  rw [Measure.compProd, ProbabilityTheory.setIntegral_compProd hs ht hf]
  simp

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