integral_compProd — Mathlib

English

If f is integrable, then ∫ z f z ∂(μ ⊗ₘ κ) = ∫ a ∫ b f(b) ∂κ(a) dμ(a).

Русский

Если функция интегрируема, то двойной интеграл от f по произведению меры равен повторному интегралу.

LaTeX

$$$$ \\int z f(z) d(μ ⊗ₘ κ) = \\int a \\int b f(b) dκ(a) dμ(a) $$$$

Lean4

theorem integral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : α × β → E} (hf : Integrable f (μ ⊗ₘ κ)) : ∫ x, f x ∂(μ ⊗ₘ κ) = ∫ a, ∫ b, f (a, b) ∂(κ a) ∂μ :=
  by
  rw [Measure.compProd, ProbabilityTheory.integral_compProd hf]
  simp

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