expGrowthSup_pow — Mathlib

English

expGrowthSup (n ↦ b^n) = log b for b ∈ ENNReal.

Русский

expGrowthSup (n ↦ b^n) = log b для b ∈ ENNReal.

LaTeX

$$$\expGrowthSup(n \mapsto b^{n}) = \log b$$$

Lean4

theorem expGrowthSup_pow : expGrowthSup (fun n ↦ b ^ n) = log b :=
  by
  rw [expGrowthSup, ← limsup_const (f := atTop (α := ℕ)) (log b)]
  refine limsup_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)
  rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n) (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm,
    log_pow, mul_comm]

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