English
If κ is a probability kernel and hf is IsRatCondKernelCDF, then for each a and x, the function b ↦ stieltjesOfMeasurableRat(f, hf.measurable, (a,b), x) is integrable with respect to ν a.
Русский
Если κ – вероятностное ядро и hf – IsRatCondKernelCDF, то для каждого a и x функция b ↦ stieltlesOfMeasurableRat(...) интегрируема по ν a.
LaTeX
$$$\\text{Integrable}\\left(b \\mapsto \\text{stieltjesOfMeasurableRat}(f, hf.measurable, (a,b), x)\\right)\\,(ν a).$$$
Lean4
theorem integrable_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) :
Integrable (fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) x) (ν a) :=
by
have :
(fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) x) = fun b ↦
(ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x)).toReal :=
by
ext t
rw [ENNReal.toReal_ofReal]
exact stieltjesOfMeasurableRat_nonneg _ _ _
rw [this]
refine integrable_toReal_of_lintegral_ne_top ?_ ?_
· refine (Measurable.ennreal_ofReal ?_).aemeasurable
exact (measurable_stieltjesOfMeasurableRat hf.measurable x).comp measurable_prodMk_left
· rw [lintegral_stieltjesOfMeasurableRat hf]
exact measure_ne_top _ _
