internlm/Lean-Github huggingface dataset:
Theorem: SuperAt.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
gc : ContinuousAt (g f d) 0
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
exact (Complex.differentiableOn_compl_singleton_and_continuousAt_iff (o.mem_nhds t0)).mp ⟨ga, gc⟩
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
h : AnalyticOn ℂ (g f d) t
⊢ AnalyticAt ℂ (g f d) c
Tactic:
rw [← ht] at h
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
h : AnalyticOn ℂ (g f d) (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
h : AnalyticOn ℂ (g f d) (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Tactic:
exact h _ (mem_ball_self rp)
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ DifferentiableOn ℂ (g f d) (t \ {0})
Tactic:
have e : ∀ z : ℂ, z ∈ t \ {0} → g f d z = f z / z ^ d := by
  intro z zs; simp only [Set.mem_diff, Set.mem_singleton_iff] at zs
  simp only [g, zs.2, if_false]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (g f d) (t \ {0})
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (g f d) (t \ {0})
Tactic:
rw [differentiableOn_congr e]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => f x / x ^ d) (t \ {0})
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => f x / x ^ d) (t \ {0})
Tactic:
apply DifferentiableOn.div (fa.mono (Set.diff_subset _ _)).differentiableOn
Proof state after:
case hd
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => x ^ d) (t \ {0})

case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0
Theorem: SuperAt.ga_of_fa
Proof state before:
case hd
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => x ^ d) (t \ {0})

case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0
Tactic:
exact (Differentiable.pow differentiable_id _).differentiableOn
Proof state after:
case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0
Theorem: SuperAt.ga_of_fa
Proof state before:
case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0
Tactic:
intro z zs
Proof state after:
case hx
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
z : ℂ
zs : z ∈ t \ {0}
⊢ z ^ d ≠ 0
Theorem: SuperAt.ga_of_fa
Proof state before:
case hx
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
z : ℂ
zs : z ∈ t \ {0}
⊢ z ^ d ≠ 0
Tactic:
exact pow_ne_zero _ (Set.mem_diff_singleton.mp zs).2
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
Tactic:
intro z zs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t \ {0}
⊢ g f d z = f z / z ^ d
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t \ {0}
⊢ g f d z = f z / z ^ d
Tactic:
simp only [Set.mem_diff, Set.mem_singleton_iff] at zs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t ∧ ¬z = 0
⊢ g f d z = f z / z ^ d
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t ∧ ¬z = 0
⊢ g f d z = f z / z ^ d
Tactic:
simp only [g, zs.2, if_false]
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
rw [Set.diff_singleton_eq_self t0] at ga
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) t
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Theorem: SuperAt.ga_of_fa
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) t
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
exact ga
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ ContinuousAt (g f d) 0
Tactic:
rw [Metric.continuousAt_iff]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < ε
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < ε
Tactic:
intro e ep
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
e : ℝ
ep : e > 0
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
e : ℝ
ep : e > 0
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e
Tactic:
rcases Metric.eventually_nhds_iff.mp
    (Asymptotics.isBigOWith_iff.mp (s.approx.forall_isBigOWith (by linarith : e / 2 > 0))) with
  ⟨t, tp, h⟩
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e
Tactic:
use t, tp
Proof state after:
case right
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∀ {x : ℂ}, dist x 0 < t → dist (g f d x) (g f d 0) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case right
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∀ {x : ℂ}, dist x 0 < t → dist (g f d x) (g f d 0) < e
Tactic:
intro z zs
Proof state after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
z : ℂ
zs : dist z 0 < t
⊢ dist (g f d z) (g f d 0) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
z : ℂ
zs : dist z 0 < t
⊢ dist (g f d z) (g f d 0) < e
Tactic:
specialize h zs
Proof state after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : ‖f z - z ^ d‖ ≤ e / 2 * ‖z ^ d‖
⊢ dist (g f d z) (g f d 0) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : ‖f z - z ^ d‖ ≤ e / 2 * ‖z ^ d‖
⊢ dist (g f d z) (g f d 0) < e
Tactic:
simp only [Complex.norm_eq_abs] at h
Proof state after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ dist (g f d z) (g f d 0) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ dist (g f d z) (g f d 0) < e
Tactic:
simp only [g, Complex.dist_eq]
Proof state after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Tactic:
simp only [z0, if_false, eq_self_iff_true, if_true]
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1) < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1) < e
Tactic:
calc
  abs (f z / z ^ d - 1) = abs (f z * (z ^ d)⁻¹ - 1) := by rw [div_eq_mul_inv]
  _ = abs ((f z - z ^ d) * (z ^ d)⁻¹) := by
    rw [mul_sub_right_distrib, mul_inv_cancel (pow_ne_zero d z0)]
  _ = abs (f z - z ^ d) * (abs (z ^ d))⁻¹ := by rw [Complex.abs.map_mul, map_inv₀]
  _ ≤ e / 2 * abs (z ^ d) * (abs (z ^ d))⁻¹ := by bound
  _ = e / 2 * (abs (z ^ d) * (abs (z ^ d))⁻¹) := by ring
  _ ≤ e / 2 * 1 := by bound
  _ = e / 2 := by ring
  _ < e := half_lt_self ep
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
e : ℝ
ep : e > 0
⊢ e / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Tactic:
simp only [z0, sub_self, AbsoluteValue.map_zero]
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ 0 < e
Theorem: SuperAt.ga_of_fa
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ 0 < e
Tactic:
exact ep
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1) = Complex.abs (f z * (z ^ d)⁻¹ - 1)
Tactic:
rw [div_eq_mul_inv]
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z * (z ^ d)⁻¹ - 1) = Complex.abs ((f z - z ^ d) * (z ^ d)⁻¹)
Tactic:
rw [mul_sub_right_distrib, mul_inv_cancel (pow_ne_zero d z0)]
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs ((f z - z ^ d) * (z ^ d)⁻¹) = Complex.abs (f z - z ^ d) * (Complex.abs (z ^ d))⁻¹
Tactic:
rw [Complex.abs.map_mul, map_inv₀]
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z - z ^ d) * (Complex.abs (z ^ d))⁻¹ ≤ e / 2 * Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ e / 2 * Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹ = e / 2 * (Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹)
Tactic:
ring
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ e / 2 * (Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹) ≤ e / 2 * 1
Tactic:
bound
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ e / 2 * 1 = e / 2
Tactic:
ring
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof 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
Proof 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
Theorem: SuperAt.super_on_ball
Proof 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
Proof 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