noncomputable def Real.iteratedLog (x : ℝ) : ℕ

The iterated logarithm of x is the number of times the natural logarithm must be iteratively applied before the result is less than or equal to 1. Reference: https://en.wikipedia.org/wiki/Iterated_logarithm

Equations

• x.iteratedLog = sInf {n : ℕ | Real.log^[n] x ≤ 1}

theorem Real.iteratedLog_eq_zero_of_le {x : ℝ} (hx : x ≤ 1) : x.iteratedLog = 0

theorem Real.iteratedLog_eq_zero_of_neg {x : ℝ} (hx : x < 0) : x.iteratedLog = 0