stieltjesFunction_le_one — Mathlib

English

For all a and real x, hf.stieltjesFunction a x ≤ 1.

Русский

Для всех a и действительных x, hf.stieltjesFunction a x ≤ 1.

LaTeX

$$$$ hf.stieltjesFunction a x ≤ 1 $$$$

Lean4

theorem stieltjesFunction_le_one (a : α) (x : ℝ) : hf.stieltjesFunction a x ≤ 1 :=
  by
  obtain ⟨r, hrx⟩ := exists_rat_gt x
  rw [← StieltjesFunction.iInf_rat_gt_eq]
  simp_rw [IsMeasurableRatCDF.stieltjesFunction_eq]
  refine ciInf_le_of_le ?_ ?_ (hf.le_one _ _)
  · refine ⟨0, fun z ↦ ?_⟩; rintro ⟨u, rfl⟩; exact hf.nonneg a _
  · exact ⟨r, hrx⟩

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