English
For any monotone f, hf.stieltjesFunction equals rightLim f.
Русский
Для монотонной f, hf.stieltjesFunction равно rightLim f.
LaTeX
$$$$ hf.stieltjesFunction = rightLim f. $$$$
Lean4
/-- If a function `f : ℝ → ℝ` is monotone, then the function mapping `x` to the right limit of `f`
at `x` is a Stieltjes function, i.e., it is monotone and right-continuous. -/
noncomputable def _root_.Monotone.stieltjesFunction {f : ℝ → ℝ} (hf : Monotone f) : StieltjesFunction
where
toFun := rightLim f
mono' _ _ hxy := hf.rightLim hxy
right_continuous' := by
intro x s hs
obtain ⟨l, u, hlu, lus⟩ : ∃ l u : ℝ, rightLim f x ∈ Ioo l u ∧ Ioo l u ⊆ s := mem_nhds_iff_exists_Ioo_subset.1 hs
obtain ⟨y, xy, h'y⟩ : ∃ (y : ℝ), x < y ∧ Ioc x y ⊆ f ⁻¹' Ioo l u :=
mem_nhdsGT_iff_exists_Ioc_subset.1 (hf.tendsto_rightLim x (Ioo_mem_nhds hlu.1 hlu.2))
change ∀ᶠ y in 𝓝[≥] x, rightLim f y ∈ s
filter_upwards [Ico_mem_nhdsGE xy] with z hz
apply lus
refine ⟨hlu.1.trans_le (hf.rightLim hz.1), ?_⟩
obtain ⟨a, za, ay⟩ : ∃ a : ℝ, z < a ∧ a < y := exists_between hz.2
calc
rightLim f z ≤ f a := hf.rightLim_le za
_ < u := (h'y ⟨hz.1.trans_lt za, ay.le⟩).2
