stieltjesFunctionAux_nonneg — Mathlib

English

For a measurable Rat-CDF f, there is a corresponding StieltjesFunction with toFun = stieltjesFunctionAux f a, monotone and right-continuous properties.

Русский

Сопутствующая функция Стилетджесса существует: для измеримой f имеется StieltjesFunction с toFun = stieltjesFunctionAux f a, а также монотонность и правую непрерывность.

LaTeX

$$$$\\text{stieltjesFunction}(a) = \\text{StieltjesFunction}\\{ toFun := \\mathrm{stieltjesFunctionAux} f a,\\; \\text{mono'} := \\text{monotone\_stieltjesFunctionAux} hf a,\\; \\text{right\_continuous'} := \\text{continuousWithinAt\_stieltjesFunctionAux\_Ici} hf a \\}.$$$$

Lean4

theorem stieltjesFunctionAux_nonneg (a : α) (r : ℝ) : 0 ≤ IsMeasurableRatCDF.stieltjesFunctionAux f a r :=
  by
  have : Nonempty { r' : ℚ // r < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt r
    exact ⟨⟨r, hrx⟩⟩
  rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]
  exact le_ciInf fun r' ↦ hf.nonneg a _

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