lintegral_id_prod — Mathlib

English

Let f: (α × β) → ℝ≥0∞ be measurable and κ: Kernel α β with IsSFiniteKernel κ. Then for a ∈ α, the lintegral with respect to Kernel.id ×ₖ κ of f equals the lintegral of f(a, b) with respect to κ a.

Русский

Пусть f: α×β → ℝ≥0∞ измеримо и κ: α → β с конечной S. Тогда линегральный интеграл по Kernel.id × κ равен интегралу по κ a от f(a, b).

LaTeX

$$$\\displaystyle \\int^{\\! -}_{p} f(p) \\, d((\\mathrm{Kernel}.id \\times_K \\kappa) a) \\\\= \\int^{\\! -}_{b} f(a, b) \\, d\\kappa(a)(b)$$$

Lean4

theorem lintegral_id_prod {f : (α × β) → ℝ≥0∞} (hf : Measurable f) (κ : Kernel α β) [IsSFiniteKernel κ] (a : α) :
    ∫⁻ p, f p ∂(Kernel.id ×ₖ κ) a = ∫⁻ b, f (a, b) ∂κ a := by
  rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]

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