monotone_stieltjesFunctionAux — Mathlib

English

For each a, the auxiliary Stieltjes function r ↦ stieltjesFunctionAux f a r is monotone in r.

Русский

Для каждого a функция r ↦ stieltjesFunctionAux f a r монотонна по r.

LaTeX

$$$$\\text{Monotone}(\\mathrm{IsMeasurableRatCDF.stieltjesFunctionAux} f a).$$$$

Lean4

theorem monotone_stieltjesFunctionAux (a : α) : Monotone (IsMeasurableRatCDF.stieltjesFunctionAux f a) :=
  by
  intro x y hxy
  have : Nonempty { r' : ℚ // y < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt y
    exact ⟨⟨r, hrx⟩⟩
  simp_rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]
  refine le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_
  · refine ⟨0, fun z ↦ ?_⟩; rintro ⟨u, rfl⟩; exact hf.nonneg a _
  · exact ⟨r.1, hxy.trans_lt r.prop⟩
  · rfl

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