tendsto_stieltjesFunction_atBot — Mathlib

English

As x goes to −∞ along real numbers, hf.stieltjesFunction a tends to 0.

Русский

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

LaTeX

$$$$ \\lim_{x \\to -\\infty} hf.stieltjesFunction a x = 0 $$$$

Lean4

theorem tendsto_stieltjesFunction_atBot (a : α) : Tendsto (hf.stieltjesFunction a) atBot (𝓝 0) :=
  by
  have h_exists : ∀ x : ℝ, ∃ q : ℚ, x < q ∧ ↑q < x + 1 := fun x ↦ exists_rat_btwn (lt_add_one x)
  let qs : ℝ → ℚ := fun x ↦ (h_exists x).choose
  have hqs_tendsto : Tendsto qs atBot atBot := by
    rw [tendsto_atBot_atBot]
    refine fun q ↦ ⟨q - 1, fun y hy ↦ ?_⟩
    have h_le : ↑(qs y) ≤ (q : ℝ) - 1 + 1 := (h_exists y).choose_spec.2.le.trans (add_le_add hy le_rfl)
    rw [sub_add_cancel] at h_le
    exact mod_cast h_le
  refine
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ((hf.tendsto_atBot_zero a).comp hqs_tendsto)
      (stieltjesFunction_nonneg hf a) fun x ↦ ?_
  rw [Function.comp_apply, ← stieltjesFunction_eq hf]
  exact (hf.stieltjesFunction a).mono (h_exists x).choose_spec.1.le

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