/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Analysis.Complex.ExponentialBounds
public import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic@[expose] public section
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
noncomputable def Real.iteratedLog (x : ℝ) : ℕ :=
sInf { (n : ℕ) | Real.log^[n] x ≤ 1 }theorem Real.iteratedLog_eq_zero_of_le {x : ℝ} (hx : x ≤ 1) :
Real.iteratedLog x = 0 := x:ℝhx:x ≤ 1⊢ x.iteratedLog = 0
All goals completed! 🐙theorem Real.iteratedLog_eq_zero_of_neg {x : ℝ} (hx : x < 0) :
Real.iteratedLog x = 0 :=
Real.iteratedLog_eq_zero_of_le (x:ℝhx:x < 0⊢ x ≤ 1 All goals completed! 🐙)this:Real.log 2 ≤ 1⊢ Nat.find ⋯ = 1
exact (Nat.find_eq_iff _).2 ⟨this, fun n hn => this:Real.log 2 ≤ 1n:ℕhn:n < 1⊢ n ∉ {x | Real.log^[x] 2 ≤ 1} All goals completed! 🐙⟩this:Real.log^[2] 4 ≤ 1⊢ Nat.find ⋯ = 2
refine (Nat.find_eq_iff _).2 ⟨this:Real.log^[2] 4 ≤ 1⊢ 2 ∈ {x | Real.log^[x] 4 ≤ 1} All goals completed! 🐙, fun n hn => ?_⟩
this:Real.log^[2] 4 ≤ 1n:ℕhn:0 < 2⊢ 0 ∉ {x | Real.log^[x] 4 ≤ 1}this:Real.log^[2] 4 ≤ 1n:ℕhn:1 < 2⊢ 1 ∉ {x | Real.log^[x] 4 ≤ 1}; this:Real.log^[2] 4 ≤ 1n:ℕhn:1 < 2⊢ 1 ∉ {x | Real.log^[x] 4 ≤ 1}
this:Real.log^[2] 4 ≤ 1n:ℕhn:1 < 2⊢ Real.exp 1 < 4
All goals completed! 🐙