Theorem: tendsto_f'_atInf (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ Tendsto (uncurry (f' d)) (𝓝 c ×ˢ atInf) atInf
Tactic:
simp only [atInf_basis.tendsto_right_iff, Complex.norm_eq_abs, Set.mem_setOf_eq,
  forall_true_left, uncurry, Metric.eventually_nhds_prod_iff]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ ∀ (i : ℝ),
    ∃ ε > 0,
      ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i_1 : ℂ}, pa i_1 → i < Complex.abs (f' d x i_1)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ ∀ (i : ℝ),
    ∃ ε > 0,
      ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i_1 : ℂ}, pa i_1 → i < Complex.abs (f' d x i_1)
Tactic:
intro r
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i : ℂ}, pa i → r < Complex.abs (f' d x i)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i : ℂ}, pa i → r < Complex.abs (f' d x i)
Tactic:
use 1, zero_lt_one, fun z ↦ max r 0 + abs c + 1 < abs z
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ (∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i) ∧
    ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ (∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i) ∧
    ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)
Tactic:
constructor
State after:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i

case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)

State before:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i
Tactic:
refine (eventually_atInf (max r 0 + abs c + 1)).mp (eventually_of_forall fun w h ↦ ?_)
State after:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : ‖w‖ > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w

State before:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : ‖w‖ > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w
Tactic:
simp only [Complex.norm_eq_abs] at h
State after:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : Complex.abs w > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w

State before:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : Complex.abs w > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w
Tactic:
exact h
State after:
no goals

State before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)
Tactic:
intro e ec z h
State after:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : dist e c < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)

State before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : dist e c < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)
Tactic:
simp only [Complex.dist_eq] at ec
State after:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)

State before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)
Tactic:
have zz : abs z ≤ abs (z ^ d) := by
  rw [Complex.abs.map_pow]
  refine le_self_pow ?_ (d_ne_zero _)
  exact le_trans (le_add_of_nonneg_left (add_nonneg (le_max_right _ _) (Complex.abs.nonneg _)))
    h.le
State after:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ r < Complex.abs (f' d e z)

State before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ r < Complex.abs (f' d e z)
Tactic:
calc abs (f' d e z)
  _ = abs (z ^ d + e) := rfl
  _ = abs (z ^ d + (c + (e - c))) := by ring_nf
  _ ≥ abs (z ^ d) - abs (c + (e - c)) := by bound
  _ ≥ abs (z ^ d) - (abs c + abs (e - c)) := by bound
  _ ≥ abs z - (abs c + 1) := by bound
  _ > max r 0 + abs c + 1 - (abs c + 1) := by bound
  _ = max r 0 := by ring_nf
  _ ≥ r := le_max_left _ _
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ Complex.abs z ≤ Complex.abs (z ^ d)
Tactic:
rw [Complex.abs.map_pow]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z ^ d

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z ^ d
Tactic:
refine le_self_pow ?_ (d_ne_zero _)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ 1 ≤ Complex.abs z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ 1 ≤ Complex.abs z
Tactic:
exact le_trans (le_add_of_nonneg_left (add_nonneg (le_max_right _ _) (Complex.abs.nonneg _)))
  h.le
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d + e) = Complex.abs (z ^ d + (c + (e - c)))
Tactic:
ring_nf
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d + (c + (e - c))) ≥ Complex.abs (z ^ d) - Complex.abs (c + (e - c))
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d) - Complex.abs (c + (e - c)) ≥ Complex.abs (z ^ d) - (Complex.abs c + Complex.abs (e - c))
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d) - (Complex.abs c + Complex.abs (e - c)) ≥ Complex.abs z - (Complex.abs c + 1)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs z - (Complex.abs c + 1) > max r 0 + Complex.abs c + 1 - (Complex.abs c + 1)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ max r 0 + Complex.abs c + 1 - (Complex.abs c + 1) = max r 0
Tactic:
ring_nf
State after:
no goals