Theorem: SuperAt.super_on_ball (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
⊢ ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
intro z z0 zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
z0 : z ≠ 0
zs : z ∈ ball 0 r
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
z0 : z ≠ 0
zs : z ∈ ball 0 r
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs, lt_min_iff] at zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
specialize gs zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (g f d z - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (g f d z - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
simp only [g, z0, if_false, eq_self_iff_true, if_true] at gs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (f z / z ^ d - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (f z / z ^ d - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
exact gs.le
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ ∀ {z : ℂ}, z ∈ ball 0 r → Complex.abs z ≤ 1 / 2
Tactic:
intro z zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ Complex.abs z ≤ 1 / 2

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ Complex.abs z ≤ 1 / 2
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs] at zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : Complex.abs z < r
⊢ Complex.abs z ≤ 1 / 2

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : Complex.abs z < r
⊢ Complex.abs z ≤ 1 / 2
Tactic:
exact le_trans zs.le r2
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ MapsTo f (ball 0 r) (ball 0 r)
Tactic:
intro z zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ f z ∈ ball 0 r

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ f z ∈ ball 0 r
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs] at zs gs ⊢
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ Complex.abs (f z) < r

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ Complex.abs (f z) < r
Tactic:
by_cases z0 : z = 0
State after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : z = 0
⊢ Complex.abs (f z) < r

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z) < r

State before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z) < r
Tactic:
calc abs (f z)
  _ = abs (f z / z ^ d * z ^ d) := by rw [div_mul_cancel₀ _ (pow_ne_zero d z0)]
  _ = abs (f z / z ^ d - 1 + 1) * abs z ^ d := by
    simp only [AbsoluteValue.map_mul, Complex.abs_pow, sub_add_cancel]
  _ ≤ (abs (f z / z ^ d - 1) + abs (1 : ℂ)) * r ^ d := by bound
  _ ≤ (1 / 4 + abs (1 : ℂ)) * r ^ d := by bound [gs z0 zs]
  _ ≤ 5 / 4 * r ^ (d - 1) * r := by
    rw [mul_assoc, ← pow_succ, Nat.sub_add_cancel (le_trans one_le_two s.d2)]; norm_num
  _ ≤ 5 / 4 * (1 / 2 : ℝ) ^ (d - 1) * r := by bound
  _ ≤ 5 / 4 * (1 / 2 : ℝ) ^ (2 - 1) * r := by bound
  _ = 5 / 8 * r := by norm_num
  _ < r := by linarith
State after:
no goals

State before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : z = 0
⊢ Complex.abs (f z) < r
Tactic:
simp only [z0, s.f0, rp, AbsoluteValue.map_zero]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z) = Complex.abs (f z / z ^ d * z ^ d)
Tactic:
rw [div_mul_cancel₀ _ (pow_ne_zero d z0)]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d * z ^ d) = Complex.abs (f z / z ^ d - 1 + 1) * Complex.abs z ^ d
Tactic:
simp only [AbsoluteValue.map_mul, Complex.abs_pow, sub_add_cancel]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1 + 1) * Complex.abs z ^ d ≤ (Complex.abs (f z / z ^ d - 1) + Complex.abs 1) * r ^ d
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (Complex.abs (f z / z ^ d - 1) + Complex.abs 1) * r ^ d ≤ (1 / 4 + Complex.abs 1) * r ^ d
Tactic:
bound [gs z0 zs]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (1 / 4 + Complex.abs 1) * r ^ d ≤ 5 / 4 * r ^ (d - 1) * r
Tactic:
rw [mul_assoc, ← pow_succ, Nat.sub_add_cancel (le_trans one_le_two s.d2)]
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (1 / 4 + Complex.abs 1) * r ^ d ≤ 5 / 4 * r ^ d

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (1 / 4 + Complex.abs 1) * r ^ d ≤ 5 / 4 * r ^ d
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 4 * r ^ (d - 1) * r ≤ 5 / 4 * (1 / 2) ^ (d - 1) * r
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 4 * (1 / 2) ^ (d - 1) * r ≤ 5 / 4 * (1 / 2) ^ (2 - 1) * r
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 4 * (1 / 2) ^ (2 - 1) * r = 5 / 8 * r
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 8 * r < r
Tactic:
linarith
State after:
no goals