lintegral_prod_id — Mathlib

English

Same as Lintegral Id-Prod above, expressing the equalities for the case f is the identity on the product index and κ is a kernel.

Русский

То же, что и выше для случая, когда f является тождественным отображением на произведение индексов и κ — ядро.

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_prod_id {f : (α × β) → ℝ≥0∞} (hf : Measurable f) (κ : Kernel β α) [IsSFiniteKernel κ] (b : β) :
    ∫⁻ p, f p ∂(κ ×ₖ Kernel.id) b = ∫⁻ a, f (a, b) ∂κ b := by
  rw [Kernel.id, lintegral_prod_deterministic _ _ _ hf, id_eq]

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