English
If two Stieltjes functions f and g have the same measure and the same left limit l at the left end, then f = g.
Русский
Если две функции Стильтьеса f и g имеют одну и ту же меру и одинаковый левый предел l на левом краю, тогда f = g.
LaTeX
$$$\\\\forall f,g\\\\in \\\\text{StieltjesFunction}, \\\\( f.\\\\mathrm{measure}= g.\\\\mathrm{measure} \\\\Rightarrow \\\\forall l \\\\in \\\\mathbb{R}, \\\\left( \\\\text{Tendsto } f \\\\ atBot \\\\ (\\\\nhds l) \\\\land \\\\text{Tendsto } g \\\\ atBot \\\\ (\\\\nhds l) \\\\right) \\\\Rightarrow f = g$$$
Lean4
theorem eq_of_measure_of_tendsto_atBot (g : StieltjesFunction) {l : ℝ} (hfg : f.measure = g.measure)
(hfl : Tendsto f atBot (𝓝 l)) (hgl : Tendsto g atBot (𝓝 l)) : f = g :=
by
ext x
have hf := measure_Iic f hfl x
rw [hfg, measure_Iic g hgl x, ENNReal.ofReal_eq_ofReal_iff, eq_comm] at hf
· simpa using hf
· rw [sub_nonneg]
exact Monotone.le_of_tendsto g.mono hgl x
· rw [sub_nonneg]
exact Monotone.le_of_tendsto f.mono hfl x
