lintegral_stieltjesOfMeasurableRat

English

Extend the set-level Stieltjes integral identity from rationals to all reals via monotone limits and measure-theoretic arguments.

Русский

Расширяем идентичность интеграла Стильтьджеса от рационалов до всех вещественных через монотонные пределы.

LaTeX

$$$\\text{setLIntegral}_{s}(\\text{stieltjesOfMeasurableRat}(f, hf.measurable,(a,b), x)) = κ(a)(s ×ˢ Iic(x)).$$$

Lean4

theorem lintegral_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) :
    ∫⁻ b, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x) ∂(ν a) = κ a (univ ×ˢ Iic x) := by
  rw [← setLIntegral_univ, setLIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

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