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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ Postcritical ⋯ c ↑z
Tactic:
have d0 : 0 < d := d_pos d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
⊢ Postcritical ⋯ c ↑z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
⊢ Postcritical ⋯ c ↑z
Tactic:
have lcz : log (log (abs c)) ≤ log (log (abs z)) := log_log_mono (by linarith) cz
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ Postcritical ⋯ c ↑z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ Postcritical ⋯ c ↑z
Tactic:
simp only [Postcritical, multibrot_p]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ ⋯.potential c ↑z < ⋯.potential c 0

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ ⋯.potential c ↑z < ⋯.potential c 0
Tactic:
set s := superF d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c ↑z < s.potential c 0

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c ↑z < s.potential c 0
Tactic:
rw [← Real.pow_rpow_inv_natCast s.potential_nonneg d0.ne', ←
  Real.pow_rpow_inv_natCast (s.potential_nonneg : 0 ≤ s.potential c 0) d0.ne']
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ (s.potential c ↑z ^ d) ^ (↑d)⁻¹ < (s.potential c 0 ^ d) ^ (↑d)⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ (s.potential c ↑z ^ d) ^ (↑d)⁻¹ < (s.potential c 0 ^ d) ^ (↑d)⁻¹
Tactic:
simp only [← s.potential_eqn]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) ^ (↑d)⁻¹ < s.potential c (f d c 0) ^ (↑d)⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) ^ (↑d)⁻¹ < s.potential c (f d c 0) ^ (↑d)⁻¹
Tactic:
refine Real.rpow_lt_rpow s.potential_nonneg ?_ (by bound)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Tactic:
generalize hw : f' d c z = w
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Tactic:
have e : f d c z = w := by rw [f, lift_coe', hw]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Tactic:
simp only [f_0, e]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c ↑w < s.potential c ↑c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
clear e
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c ↑w < s.potential c ↑c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have zw : abs z ≤ abs w := by rw [←hw]; exact le_self_iter d (by linarith) cz 1
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have cw : abs c ≤ abs w := le_trans cz zw
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have pc1 : s.potential c c < 1 := potential_lt_one_of_two_lt (by linarith) (le_refl _)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ s.potential c ↑w < s.potential c ↑c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have pw1 : s.potential c w < 1 := potential_lt_one_of_two_lt (by linarith) (by linarith)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ s.potential c ↑w < s.potential c ↑c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
rw [←log_neg_log_strict_anti potential_pos potential_pos pw1 pc1]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < (-(⋯.potential c ↑w).log).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < (-(⋯.potential c ↑w).log).log
Tactic:
refine lt_of_lt_of_le ?_ (le_sub_iff_add_le.mp (abs_le.mp
  (log_neg_log_potential_approx d (by linarith) cw)).1)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < -iter_error d c w + (Complex.abs w).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
refine lt_of_le_of_lt (sub_le_iff_le_add.mp (abs_le.mp
  (log_neg_log_potential_approx d (by linarith) (le_refl _))).2) ?_
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have lzw : log (log (abs z)) + 0.548 ≤ log (log (abs w)) := by
  rw [←hw]; exact log_log_iter (by linarith) cz
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have ie : ∀ z : ℂ, 4 ≤ abs z → abs c ≤ abs z → iter_error d c z ≤ 0.15 := by
  intro z z4 cz
  refine le_trans (iter_error_le_of_z4 d z4 cz) ?_
  calc 0.8095 / (abs z * log (abs z))
    _ ≤ 0.8095 / (4 * log 4) := by bound
    _ ≤ 0.8095 / (4 * 1.386) := by bound [lt_log_4]
    _ ≤ 0.15 := by norm_num
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have iec := ie c c4 (le_refl _)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have iew := ie w (by linarith) cw
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
refine lt_of_lt_of_le (lt_of_le_of_lt (add_le_add iec lcz) ?_) (add_le_add (neg_le_neg iew) lzw)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 0.15 + (Complex.abs z).log.log < -0.15 + ((Complex.abs z).log.log + 0.548)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 0.15 + (Complex.abs z).log.log < -0.15 + ((Complex.abs z).log.log + 0.548)
Tactic:
ring_nf
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 + (Complex.abs z).log.log < 199 / 500 + (Complex.abs z).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 + (Complex.abs z).log.log < 199 / 500 + (Complex.abs z).log.log
Tactic:
simp only [add_lt_add_iff_right]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 < 199 / 500

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 < 199 / 500
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
⊢ 1 < Complex.abs c
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ 0 < (↑d)⁻¹
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ f d c ↑z = ↑w
Tactic:
rw [f, lift_coe', hw]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ Complex.abs z ≤ Complex.abs w
Tactic:
rw [←hw]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ Complex.abs z ≤ Complex.abs (f' d c z)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ Complex.abs z ≤ Complex.abs (f' d c z)
Tactic:
exact le_self_iter d (by linarith) cz 1
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ 3 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ 2 < Complex.abs c
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ 2 < Complex.abs w
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ Complex.abs c ≤ Complex.abs w
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ 3 ≤ Complex.abs w
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ 3 ≤ Complex.abs c
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
Tactic:
rw [←hw]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs (f' d c z)).log.log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs (f' d c z)).log.log
Tactic:
exact log_log_iter (by linarith) cz
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ 4 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
⊢ ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
Tactic:
intro z z4 cz
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.15

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.15
Tactic:
refine le_trans (iter_error_le_of_z4 d z4 cz) ?_
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.15

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.15
Tactic:
calc 0.8095 / (abs z * log (abs z))
  _ ≤ 0.8095 / (4 * log 4) := by bound
  _ ≤ 0.8095 / (4 * 1.386) := by bound [lt_log_4]
  _ ≤ 0.15 := by norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.8095 / (4 * log 4)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (4 * log 4) ≤ 0.8095 / (4 * 1.386)
Tactic:
bound [lt_log_4]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (4 * 1.386) ≤ 0.15
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
⊢ 4 ≤ Complex.abs w
Tactic:
linarith
State after:
no goals