lintegral_compProd — Mathlib

English

For measurable f: α × β → ℝ≥0∞, the lintegral w.r.t. μ ⊗ₘ κ equals the iterated lintegral: ∫ f d(μ ⊗ₘ κ) = ∫ a ∫ b f(a,b) dκ(a) dμ.

Русский

Для измеримой функции f: α × β → ℝ≥0∞ выполняется: ∫ f d(μ ⊗ₘ κ) = ∫_α ∫_β f(a,b) dκ(a) dμ.

LaTeX

$$$\\int^- x, f x \\, d(μ ⊗_m κ) = \\int^- a, \\int^- b, f(a,b) \\, d(κ a) \\, dμ$$$

Lean4

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

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