Theorem: fast_series_converge (Ray/Analytic/Series.lean)

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ ∃ g, AnalyticOn ℂ g s ∧ HasSumOn f g s
Tactic:
use tsumOn f
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s ∧ HasSumOn f (tsumOn f) s

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s ∧ HasSumOn f (tsumOn f) s
Tactic:
constructor
State after:
case h.left
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s

case h.right
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ HasSumOn f (tsumOn f) s

State before:
case h.left
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s
Tactic:
exact uniform_analytic_lim o (fun N ↦ N.analyticOn_sum fun _ _ ↦ h _)
  (fast_series_converge_uniformly_on a0 a1 hf)
State after:
no goals

State before:
case h.right
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ HasSumOn f (tsumOn f) s
Tactic:
exact fun z zs ↦ Summable.hasSum (fast_series_converge_at a0 a1 fun n ↦ hf n z zs)
State after:
no goals