English
If two Stieltjes functions have the same measure and agree at a single point y, then the two functions are equal.
Русский
Если две функции Стильтьеса имеют одну и ту же меру и совпадают в одной точке y, то функции совпадают на всю область.
LaTeX
$$$\\\\forall f,g \\\\in \\\\text{StieltjesFunction}, \\\\text{Eq}(f.\\\\mathrm{measure}, g.\\\\mathrm{measure}) \\\\Rightarrow \\\\exists y: f(y)=g(y) \\\\Rightarrow f=g$$$
Lean4
theorem eq_of_measure_of_eq (g : StieltjesFunction) {y : ℝ} (hfg : f.measure = g.measure) (hy : f y = g y) : f = g :=
by
ext x
cases le_total x y with
| inl hxy =>
have hf := measure_Ioc f x y
rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
· simpa using hf
· rw [sub_nonneg]
exact g.mono hxy
· rw [sub_nonneg]
exact f.mono hxy
| inr hxy =>
have hf := measure_Ioc f y x
rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
· simpa using hf
· rw [sub_nonneg]
exact g.mono hxy
· rw [sub_nonneg]
exact f.mono hxy
