Theorem: not_multibrot_of_two_lt (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
⊢ c ∉ multibrot d
Tactic:
by_cases c2 : 2 < abs c
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : 2 < Complex.abs c
⊢ c ∉ multibrot d

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : 2 < Complex.abs c
⊢ c ∉ multibrot d

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d
Tactic:
exact multibrot_two_lt c2
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d
Tactic:
simp only [multibrot_coe, not_not]
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
simp only [not_lt] at c2
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
generalize hs : abs ((f' d c)^[n] c) = s
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
s : ℝ
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
s : ℝ
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
rw [hs] at h
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
have s1 : 1 ≤ s := by linarith
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
have s1' : 1 ≤ s - 1 := by linarith
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
have s0 : 0 ≤ s := by linarith
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
simp only [tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs]
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] c)) atTop atTop

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] c)) atTop atTop
Tactic:
rw [← Filter.tendsto_add_atTop_iff_nat n]
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n_1 => Complex.abs ((f' d c)^[n_1 + n] c)) atTop atTop

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n_1 => Complex.abs ((f' d c)^[n_1 + n] c)) atTop atTop
Tactic:
apply Filter.tendsto_atTop_mono b
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => s * (s - 1) ^ n) atTop atTop

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => s * (s - 1) ^ n) atTop atTop
Tactic:
refine Filter.Tendsto.mul_atTop (by linarith) tendsto_const_nhds ?_
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => (s - 1) ^ n) atTop atTop

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => (s - 1) ^ n) atTop atTop
Tactic:
apply tendsto_pow_atTop_atTop_of_one_lt
State after:
case neg.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ 1 < s - 1

State before:
case neg.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ 1 < s - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ 1 ≤ s
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
⊢ 1 ≤ s - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
⊢ 0 ≤ s
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
Tactic:
intro k
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
⊢ s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
⊢ s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
Tactic:
induction' k with k p
State after:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ s * (s - 1) ^ 0 ≤ Complex.abs ((f' d c)^[0 + n] c)

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs ((f' d c)^[k + 1 + n] c)

State before:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ s * (s - 1) ^ 0 ≤ Complex.abs ((f' d c)^[0 + n] c)
Tactic:
simp only [pow_zero, mul_one, zero_add, Nat.zero_eq, hs, le_refl]
State after:
no goals

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs ((f' d c)^[k + 1 + n] c)
Tactic:
simp only [Nat.succ_add, Function.iterate_succ_apply']
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c ((f' d c)^[k + n] c))

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c ((f' d c)^[k + n] c))
Tactic:
generalize hz : (f' d c)^[k + n] c = z
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
z : ℂ
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
z : ℂ
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
rw [hz] at p
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
have ss1 : 1 ≤ s * (s - 1) ^ k := by bound
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
have k2 : k ≤ k * 2 := by linarith
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
calc abs (f' d c z)
  _ = abs (z ^ d + c) := rfl
  _ ≥ abs (z ^ d) - abs c := by bound
  _ = abs z ^ d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ (s * (s - 1) ^ k) ^ d - 2 := by bound
  _ ≥ (s * (s - 1) ^ k) ^ 2 - 2 := by bound
  _ = s ^ 2 * (s - 1) ^ (k * 2) - 2 * 1 := by rw [mul_pow, pow_mul, mul_one]
  _ ≥ s ^ 2 * (s - 1) ^ k - s * (s - 1) ^ k := by bound
  _ = s * ((s - 1) ^ k * (s - 1)) := by ring
  _ = s * (s - 1) ^ (k + 1) := by rw [pow_succ]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
⊢ 1 ≤ s * (s - 1) ^ k
Tactic:
bound
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
⊢ k ≤ k * 2
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ Complex.abs (z ^ d + c) ≥ Complex.abs (z ^ d) - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ Complex.abs (z ^ d) - Complex.abs c = Complex.abs z ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ Complex.abs z ^ d - Complex.abs c ≥ (s * (s - 1) ^ k) ^ d - 2
Tactic:
bound
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ (s * (s - 1) ^ k) ^ d - 2 ≥ (s * (s - 1) ^ k) ^ 2 - 2
Tactic:
bound
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ (s * (s - 1) ^ k) ^ 2 - 2 = s ^ 2 * (s - 1) ^ (k * 2) - 2 * 1
Tactic:
rw [mul_pow, pow_mul, mul_one]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s ^ 2 * (s - 1) ^ (k * 2) - 2 * 1 ≥ s ^ 2 * (s - 1) ^ k - s * (s - 1) ^ k
Tactic:
bound
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s ^ 2 * (s - 1) ^ k - s * (s - 1) ^ k = s * ((s - 1) ^ k * (s - 1))
Tactic:
ring
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s * ((s - 1) ^ k * (s - 1)) = s * (s - 1) ^ (k + 1)
Tactic:
rw [pow_succ]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ 0 < s
Tactic:
linarith
State after:
no goals