tendsto_stieltjesFunction_atTop — Mathlib

English

As x tends to +∞, hf.stieltjesFunction a x tends to 1.

Русский

При x → +∞ функция hf.stieltjesFunction a x стремится к 1.

LaTeX

$$$$ \\lim_{x \\to +\\infty} hf.stieltjesFunction a x = 1 $$$$

Lean4

theorem tendsto_stieltjesFunction_atTop (a : α) : Tendsto (hf.stieltjesFunction a) atTop (𝓝 1) :=
  by
  have h_exists : ∀ x : ℝ, ∃ q : ℚ, x - 1 < q ∧ ↑q < x := fun x ↦ exists_rat_btwn (sub_one_lt x)
  let qs : ℝ → ℚ := fun x ↦ (h_exists x).choose
  have hqs_tendsto : Tendsto qs atTop atTop := by
    rw [tendsto_atTop_atTop]
    refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩
    have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le
    rw [sub_le_iff_le_add] at h_le
    exact_mod_cast le_of_add_le_add_right (hy.trans h_le)
  refine
    tendsto_of_tendsto_of_tendsto_of_le_of_le ((hf.tendsto_atTop_one a).comp hqs_tendsto) tendsto_const_nhds ?_
      (stieltjesFunction_le_one hf a)
  intro x
  rw [Function.comp_apply, ← stieltjesFunction_eq hf]
  exact (hf.stieltjesFunction a).mono (le_of_lt (h_exists x).choose_spec.2)

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