inverse_one_sub_norm — Mathlib

English

The map t ↦ (1 − t)⁻¹ is bounded near t = 0; more precisely, it belongs to O_{nhds 0}(1).

Русский

Отображение t ↦ (1 − t)⁻¹ ограничено около t = 0; точнее, принадлежит к O_{nhds 0}(1).

LaTeX

$$$ (t \mapsto (1-t)^{-1}) =O_{\,nhds(0)} 1 $$$

Lean4

theorem inverse_one_sub_norm : (fun t : R => inverse (1 - t)) =O[𝓝 0] (fun _t => 1 : R → ℝ) :=
  by
  simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
  refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by simp, fun t ht ↦ ?_⟩
  rw [dist_zero_right] at ht
  have ht' : ‖t‖ < 1 := by linarith
  simp only [inverse_one_sub t ht', norm_one, mul_one]
  change ‖∑' n : ℕ, t ^ n‖ ≤ _
  have := tsum_geometric_le_of_norm_lt_one t ht'
  have : (1 - ‖t‖)⁻¹ ≤ 2 := inv_le_of_inv_le₀ (by simp) (by linarith)
  linarith

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