Theorem: tendsto_log_neg_log_potential (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(⋯.potential c ↑z).log).log)
Tactic:
set s := superF d
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have zn1 : ∀ {n}, 1 < abs ((f' d c)^[n] z) := by
  intro n; exact lt_of_lt_of_le (by norm_num) (le_trans z3 (le_self_iter d z3 cz _))
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have zn0 : ∀ {n}, 0 < abs ((f' d c)^[n] z) := fun {_} ↦ lt_trans zero_lt_one zn1
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have ln0 : ∀ {n}, 0 < log (abs ((f' d c)^[n] z)) := fun {_} ↦ Real.log_pos zn1
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have dn0 : ∀ {n}, (d:ℝ)^n ≠ 0 := fun {_} ↦ pow_ne_zero _ (Nat.cast_ne_zero.mpr (d_ne_zero d))
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have p0 : 0 < s.potential c z := potential_pos
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have p1 : s.potential c z < 1 := potential_lt_one_of_two_lt (by linarith) cz
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
set f := fun x ↦ log (log x⁻¹)
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have fc : ContinuousAt f ((superF d).potential c z) := by
  refine ((NormedField.continuousAt_inv.mpr p0.ne').log (inv_ne_zero p0.ne')).log ?_
  exact Real.log_ne_zero_of_pos_of_ne_one (inv_pos.mpr p0) (inv_ne_one.mpr p1.ne)
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
fc : ContinuousAt f (⋯.potential c ↑z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
fc : ContinuousAt f (⋯.potential c ↑z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have t := Tendsto.comp fc (tendsto_potential d z3 cz)
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
fc : ContinuousAt f (⋯.potential c ↑z)
t : Tendsto (f ∘ fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (f (⋯.potential c ↑z)))
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
fc : ContinuousAt f (⋯.potential c ↑z)
t : Tendsto (f ∘ fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (f (⋯.potential c ↑z)))
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
simpa only [Real.log_inv, Real.log_neg_eq_log, Nat.cast_pow, Function.comp_def, Real.log_rpow zn0,
  neg_mul, ← div_eq_inv_mul, Real.log_div ln0.ne' dn0, Real.log_pow, f] using t
State after:
no goals

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
Tactic:
intro n
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
n : ℕ
⊢ 1 < Complex.abs ((f' d c)^[n] z)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
n : ℕ
⊢ 1 < Complex.abs ((f' d c)^[n] z)
Tactic:
exact lt_of_lt_of_le (by norm_num) (le_trans z3 (le_self_iter d z3 cz _))
State after:
no goals

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
n : ℕ
⊢ 1 < 3
Tactic:
norm_num
State after:
no goals

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
⊢ 2 < Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ ContinuousAt f (⋯.potential c ↑z)
Tactic:
refine ((NormedField.continuousAt_inv.mpr p0.ne').log (inv_ne_zero p0.ne')).log ?_
State after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ (s.potential c ↑z)⁻¹.log ≠ 0

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ (s.potential c ↑z)⁻¹.log ≠ 0
Tactic:
exact Real.log_ne_zero_of_pos_of_ne_one (inv_pos.mpr p0) (inv_ne_one.mpr p1.ne)
State after:
no goals