Theorem: bottcher_hasDerivAt_one (Ray/Dynamics/Multibrot/Bottcher.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HasDerivAt (fun z => bottcher d (↑z)⁻¹) 1 0
Tactic:
rw [HasDerivAt, HasDerivAtFilter, bottcher, hasFDerivAtFilter_iff_isLittleO, coe_zero, inv_zero',
  fill_inf]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - 0 - (ContinuousLinearMap.smulRight 1 1) (x' - 0)) =o[𝓝 0] fun x' => x' - 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - 0 - (ContinuousLinearMap.smulRight 1 1) (x' - 0)) =o[𝓝 0] fun x' => x' - 0
Tactic:
simp only [sub_zero, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
  smul_eq_mul, mul_one]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - x') =o[𝓝 0] fun x' => x'

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - x') =o[𝓝 0] fun x' => x'
Tactic:
rw [Asymptotics.isLittleO_iff]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ c * ‖x‖

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ c * ‖x‖
Tactic:
intro k k0
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ k * ‖x‖

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ k * ‖x‖
Tactic:
rw [Metric.eventually_nhds_iff]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∃ ε > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∃ ε > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖
Tactic:
refine ⟨min 16⁻¹ (k / 16), by bound, ?_⟩
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ ⦃y : ℂ⦄, dist y 0 < min 16⁻¹ (k / 16) → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ ⦃y : ℂ⦄, dist y 0 < min 16⁻¹ (k / 16) → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖
Tactic:
intro z le
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : dist z 0 < min 16⁻¹ (k / 16)
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : dist z 0 < min 16⁻¹ (k / 16)
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖
Tactic:
simp only [Complex.dist_eq, sub_zero, lt_min_iff] at le
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖
Tactic:
simp only [Complex.norm_eq_abs]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Tactic:
by_cases z0 : z = 0
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Tactic:
simp only [inv_coe z0, fill_coe]
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Tactic:
have b : abs (bottcher' d z⁻¹ - z⁻¹⁻¹) ≤ (16:ℝ) * (abs z⁻¹)⁻¹ ^ 2 := bottcher_approx d ?_
State after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z⁻¹⁻¹) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z

case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ 16 < Complex.abs z⁻¹

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ min 16⁻¹ (k / 16) > 0
Tactic:
bound
State after:
no goals

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Tactic:
simp only [z0, coe_zero, inv_zero', fill_inf, sub_zero, Complex.abs.map_zero,
  MulZeroClass.mul_zero, le_refl]
State after:
no goals

State before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z⁻¹⁻¹) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Tactic:
simp only [inv_inv] at b
State after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z

State before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Tactic:
apply le_trans b
State after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2 ≤ k * Complex.abs z

State before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2 ≤ k * Complex.abs z
Tactic:
simp only [map_inv₀, inv_inv, pow_two, ← mul_assoc]
State after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z * Complex.abs z ≤ k * Complex.abs z

State before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z * Complex.abs z ≤ k * Complex.abs z
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (Complex.abs.nonneg _)
State after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z ≤ k

State before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z ≤ k
Tactic:
calc 16 * abs z
  _ ≤ 16 * (k / 16) := by linarith [le.2]
  _ = k := by ring
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z ≤ 16 * (k / 16)
Tactic:
linarith [le.2]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * (k / 16) = k
Tactic:
ring
State after:
no goals

State before:
case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ 16 < Complex.abs z⁻¹
Tactic:
rw [map_inv₀, lt_inv (by norm_num) (Complex.abs.pos_iff.mpr z0)]
State after:
case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs z < 16⁻¹

State before:
case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs z < 16⁻¹
Tactic:
exact le.1
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals