Theorem: iter_large_z3 (Ray/Dynamics/Multibrot/Iterates.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
rw [(by norm_num : (2:ℝ) = 3-1)]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (3 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (3 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
exact iter_large d 3 (by norm_num) z3 cz n
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 = 3 - 1
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 ≤ 3
Tactic:
norm_num
State after:
no goals