English
For any a and x, the auxiliary Stieltjes function is continuous from the right at x when restricted to the interval [x, ∞).
Русский
Для любых a и x вспомогательная функция Стилетджесса непрерывна слева на правой границе x, при ограничении к интервалу [x, ∞).
LaTeX
$$$$\\text{ContinuousWithinAt}(\\mathrm{IsMeasurableRatCDF.stieltjesFunctionAux} f a) (\\mathrm{Ici} \\, x) \\, x.$$$$
Lean4
theorem continuousWithinAt_stieltjesFunctionAux_Ici (a : α) (x : ℝ) :
ContinuousWithinAt (IsMeasurableRatCDF.stieltjesFunctionAux f a) (Ici x) x :=
by
rw [← continuousWithinAt_Ioi_iff_Ici]
convert Monotone.tendsto_nhdsGT (monotone_stieltjesFunctionAux hf a) x
rw [sInf_image']
have h' : ⨅ r : Ioi x, stieltjesFunctionAux f a r = ⨅ r : { r' : ℚ // x < r' }, stieltjesFunctionAux f a r :=
by
refine Real.iInf_Ioi_eq_iInf_rat_gt x ?_ (monotone_stieltjesFunctionAux hf a)
refine ⟨0, fun z ↦ ?_⟩
rintro ⟨u, -, rfl⟩
exact stieltjesFunctionAux_nonneg hf a u
have h'' : ⨅ r : { r' : ℚ // x < r' }, stieltjesFunctionAux f a r = ⨅ r : { r' : ℚ // x < r' }, f a r :=
by
congr with r
exact stieltjesFunctionAux_eq hf a r
rw [h', h'', ContinuousWithinAt]
congr!
rw [stieltjesFunctionAux_def]
