Theorem: log_log_iter (Ray/Dynamics/Multibrot/Postcritical.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
zw : (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ Complex.abs (f' d c z)
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs (f' d c z)).log.log
Tactic:
generalize abs (f' d c z) = w at zw
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
w : ℝ
zw : (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ w
⊢ (Complex.abs z).log.log + 0.548 ≤ w.log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
w : ℝ
zw : (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ w
⊢ (Complex.abs z).log.log + 0.548 ≤ w.log.log
Tactic:
generalize abs z = x at zw cz z4
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
cz : Complex.abs c ≤ x
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
cz : Complex.abs c ≤ x
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
clear z c cz
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have x0 : 0 < x := by linarith
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have x1 : 1 < x := by linarith
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
simp only [pow_one] at zw
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have lx1 : 1 < log (x-1) :=
  lt_trans (by norm_num) (lt_of_lt_of_le lt_log_3 (Real.log_le_log (by norm_num) (by linarith)))
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have lx : 1 < log x := lt_trans lx1 (Real.log_lt_log (by linarith) (by linarith))
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have ll0 : 0 ≤ log (x-1) / log x := by positivity
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have ll1 : log (x-1) / log x ≤ 1 :=
  div_le_one_of_le (Real.log_le_log (by linarith) (by linarith)) (by positivity)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + 0.548 ≤ w.log.log

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
calc log (log w)
  _ ≥ log (log ((x-1)*x)) := log_log_mono (by nlinarith) zw
  _ = log (log x + log (x-1)) := by rw [mul_comm, Real.log_mul (by positivity) (by linarith)]
  _ = log (log x) + log (1 + log (x-1) / log x) := by rw [log_add _ _ (by linarith) (by linarith)]
  _ ≥ log (log x) + log 2 * (log (x-1) / log x) := by bound [le_log_one_add ll0 ll1]
  _ ≥ log (log x) + 0.693 * 0.791 := by bound [lt_log_2]
  _ ≥ log (log x) + 0.548 := by bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ Complex.abs (f' d c z)
Tactic:
refine iter_large (d := d) (n := 1) ?_ ?_ ?_ cz
State after:
case refine_1
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 2 ≤ Complex.abs z

case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z

State before:
case refine_1
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 2 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z
Tactic:
exact le_refl _
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
⊢ 0 < x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
⊢ 1 < x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ 1 < 1.098
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ 3 ≤ x - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ 0 < x - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ x - 1 < x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ (x - 1).log / x.log ≥ (4 - 1).log / log 4
Tactic:
apply log_ratio_mono ?_ ?_ z4
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 4 ∈ Ici 2

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ x ∈ Ici 2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 4 ∈ Ici 2
Tactic:
simp only [mem_Ici]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ 4

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ 4
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ x ∈ Ici 2
Tactic:
simp only [mem_Ici]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ (4 - 1).log / log 4 = log 3 / log 4
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 0 ≤ log 3
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 0 < log 4
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 1.098 / 1.387 ≥ 0.791
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
⊢ 0 ≤ (x - 1).log / x.log
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ 0 < x - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ x - 1 ≤ x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ 0 ≤ x.log
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ 1 < (x - 1) * x
Tactic:
nlinarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ ((x - 1) * x).log.log = (x.log + (x - 1).log).log
Tactic:
rw [mul_comm, Real.log_mul (by positivity) (by linarith)]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x ≠ 0
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x - 1 ≠ 0
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ (x.log + (x - 1).log).log = x.log.log + (1 + (x - 1).log / x.log).log
Tactic:
rw [log_add _ _ (by linarith) (by linarith)]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ 0 < x.log
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ 0 < x.log + (x - 1).log
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + (1 + (x - 1).log / x.log).log ≥ x.log.log + log 2 * ((x - 1).log / x.log)
Tactic:
bound [le_log_one_add ll0 ll1]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + log 2 * ((x - 1).log / x.log) ≥ x.log.log + 0.693 * 0.791
Tactic:
bound [lt_log_2]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + 0.693 * 0.791 ≥ x.log.log + 0.548
Tactic:
bound
State after:
no goals