stieltjesFunctionAux_eq — Mathlib

English

If hf is a measurable Rat-CDF, then for any a and rational r, the auxiliary Stieltjes function value equals f a r.

Русский

Если hf является измеримой Rat-CDF, то для любых a и рационального r значение вспомогательной функции Стилетджесса равно f a r.

LaTeX

$$$$ \\mathrm{IsMeasurableRatCDF.stieltlesFunctionAux} f a r = f a r$$$$

Lean4

theorem stieltjesFunctionAux_eq (a : α) (r : ℚ) : IsMeasurableRatCDF.stieltjesFunctionAux f a r = f a r :=
  by
  rw [← hf.iInf_rat_gt_eq a r, IsMeasurableRatCDF.stieltjesFunctionAux]
  refine Equiv.iInf_congr ?_ ?_
  ·
    exact
      { toFun := fun t ↦ ⟨t.1, mod_cast t.2⟩
        invFun := fun t ↦ ⟨t.1, mod_cast t.2⟩
        left_inv := fun t ↦ by simp only [Subtype.coe_eta]
        right_inv := fun t ↦ by simp only [Subtype.coe_eta] }
  · intro t
    simp only [Equiv.coe_fn_mk, Subtype.coe_mk]

Похожие утверждения