English
The base-b logarithm is continuous as a function from nonzero reals to reals.
Русский
Логарифм по основанию b непрерывен как функция от непустых нулей в множество значений.
LaTeX
$$$\logb b: \mathbb{R} \setminus \{0\} \to \mathbb{R} \\text{ is continuous }$$$
Lean4
/-- The function `|logb b x|` tends to `+∞` as `x` tendsto `+∞`.
See also `tendsto_logb_atTop` and `tendsto_logb_atTop_of_base_lt_one`.
-/
theorem tendsto_abs_logb_atTop (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) : Tendsto (|logb b ·|) atTop atTop :=
by
wlog hb₀ : 0 < b generalizing b
· exact (this (b := -b) (by simp [hb, neg_eq_iff_eq_neg]) (by linarith +splitNe)).congr (by simp)
wlog hb₁ : 1 < b generalizing b
·
exact
(this (b := b⁻¹) (by simp [hb, inv_eq_iff_eq_inv, inv_neg]) (by simpa)
((one_lt_inv₀ hb₀).2 (by linarith +splitNe))).congr
(by simp)
refine (tendsto_logb_atTop hb₁).congr' ?_
filter_upwards [eventually_ge_atTop 1] with x hx₁
rw [abs_of_nonneg]
exact logb_nonneg hb₁ hx₁
