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

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 3 ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
rw [(by norm_num : (3:ℝ) = 4-1)]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (4 - 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 : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (4 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
exact iter_large d 4 (by norm_num) z4 cz n
State after:
no goals

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

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