integral_condKernel — Mathlib

English

Same as Kernel Integral: for integrable f, the iterated kernel integral equals the total integral.

Русский

То же самое, что и ранее: для интегрируемой f равенство двойных интегралов.

LaTeX

$$$\\int b, \\int \\omega, f(b,\\omega) \\, \\partial(\\rho.condKernel b) \\partial\\rho.fst = \\int x, f x \\, \\partial\\rho$$$

Lean4

theorem integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) :
    Integrable (fun x ↦ ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst :=
  (integrable_norm_iff hf_int.1.integral_condKernel).mp hf_int.norm_integral_condKernel

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