lintegral — Mathlib

English

Let hf be IsCondKernelCDF; then for any a and measurable s, the lintegral over s of f(a,b)x equals the κ measure on s×Iic x.

Русский

Для hf IsCondKernelCDF лин. интеграл по s от f(a,b)x равен мере κ(a) на s×Iic x.

LaTeX

$$$\text{setLIntegral}(hf,a,s,x):= \int_{b\in s} ((f(a,b)).toFun x)\, d(ν a)(b) = (κ a).real(s ×ˢ Iic x).$$$

Lean4

theorem lintegral [IsFiniteKernel κ] {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) :
    ∫⁻ b, ENNReal.ofReal (f (a, b) x) ∂(ν a) = κ a (univ ×ˢ Iic x) := by
  rw [← hf.setLIntegral _ MeasurableSet.univ, Measure.restrict_univ]

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