stieltjesFunction — Mathlib

English

If hf is a measurable Rat-CDF, then for any a and rational r, hf.stieltjesFunction a r = f a r.

Русский

Если hf измерим, то hf.stieltjesFunction a r = f a r для любых a и рационального r.

LaTeX

$$$$ hf.stieltjesFunction a r = f a r $$$$

Lean4

/-- Extend a function `f : α → ℚ → ℝ` with property `IsMeasurableRatCDF` from `ℚ` to `ℝ`,
to a function `α → StieltjesFunction`. -/
noncomputable def stieltjesFunction (a : α) : StieltjesFunction
    where
  toFun := stieltjesFunctionAux f a
  mono' := monotone_stieltjesFunctionAux hf a
  right_continuous' x := continuousWithinAt_stieltjesFunctionAux_Ici hf a x

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