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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (c, ↑z) ∈ ⋯.basin
Tactic:
simp only [multibrot_coe, not_le, not_not, (superF d).basin_iff_attracts, Attracts, f_f'_iter,
  tendsto_inf_iff_tendsto_atInf, tendsto_atInf_iff_norm_tendsto_atTop,
  Complex.norm_eq_abs] at z2 ⊢
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] z)) atTop atTop

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] z)) atTop atTop
Tactic:
apply Filter.tendsto_atTop_mono (iter_large d (abs z) z2.le (le_refl _) cz)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n * Complex.abs z) atTop atTop

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n * Complex.abs z) atTop atTop
Tactic:
refine Filter.Tendsto.atTop_mul (by linarith) ?_ tendsto_const_nhds
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n) atTop atTop

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n) atTop atTop
Tactic:
apply tendsto_pow_atTop_atTop_of_one_lt
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1 < Complex.abs z - 1

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1 < Complex.abs z - 1
Tactic:
linarith
State after:
no goals

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