English
If -1 < b < 1, then b^x → 0 as x → ∞.
Русский
Если -1 < b < 1, то b^x → 0 при x → ∞.
LaTeX
$$$\forall b\in(-1,1),\; \lim_{x\to\infty} b^{x} = 0.$$$
Lean4
theorem tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b < 1) :
Tendsto (b ^ · : ℝ → ℝ) atTop (𝓝 (0 : ℝ)) :=
by
rcases lt_trichotomy b 0 with hb | rfl | hb
case inl => -- b < 0
simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
refine IsLittleO.mul_isBigO ?exp ?cos
case exp =>
rw [isLittleO_const_iff one_ne_zero]
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
rw [← log_neg_eq_log, log_neg_iff (by linarith)]
linarith
case cos =>
rw [isBigO_iff]
exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩
case inr.inl => -- b = 0
refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
rw [tendsto_pure]
filter_upwards [eventually_ne_atTop 0] with _ hx
simp [hx]
case inr.inr => -- b > 0
simp_rw [Real.rpow_def_of_pos hb]
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
exact (log_neg_iff hb).mpr hb₁
