setLIntegral_stieltjesOfMeasurableRat_rat

English

Extend the rat-case result to x ∈ R by a monotone convergence argument; the real-valued integral equals kernel real measure on Iic(x).

Русский

Расширяем результат для q∈ℚ до x∈ℝ через монотонную схождение; линтеграл равен мере ядра на Iic(x).

LaTeX

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

Lean4

theorem setLIntegral_stieltjesOfMeasurableRat_rat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ)
    {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ b in s, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) q) ∂(ν a) = κ a (s ×ˢ Iic (q : ℝ)) :=
  by
  rw [← ofReal_integral_eq_lintegral_ofReal]
  · rw [setIntegral_stieltjesOfMeasurableRat_rat hf a q hs, ofReal_measureReal]
  · refine Integrable.restrict ?_
    rw [integrable_congr (stieltjesOfMeasurableRat_ae_eq hf a q)]
    exact hf.integrable a q
  · exact ae_of_all _ (fun x ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

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