setLIntegral — Mathlib

English

For IsCondKernelCDF, the linar integral over b of ENNReal.ofReal((f(a,b)).toFun x) equals the real-valued kernel κ a on sets s×Iic x.

Русский

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

LaTeX

$$$\text{lintegral}_{b} \mathrm{ENNReal.ofReal}\bigl((f(a,b)).\text{toFun}(x)\bigr) \partial(\nu a) = (κ a).real\bigl(s × I_i c x\bigr).$$$

Lean4

theorem setLIntegral [IsFiniteKernel κ] {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) {s : Set β}
    (hs : MeasurableSet s) (x : ℝ) : ∫⁻ b in s, ENNReal.ofReal (f (a, b) x) ∂(ν a) = κ a (s ×ˢ Iic x) := by
  rw [← ofReal_integral_eq_lintegral_ofReal (hf.integrable a x).restrict (ae_of_all _ (fun _ ↦ hf.nonneg _ _)),
    hf.setIntegral a hs x, ofReal_measureReal]

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