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

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
⊢ Summable f
Tactic:
set s : Set ℂ := {0}
State after:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
⊢ Summable f

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
⊢ Summable f
Tactic:
set g : ℕ → ℂ → ℂ := fun n _ ↦ f n
State after:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
⊢ Summable f

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
⊢ Summable f
Tactic:
have hg : ∀ n z, z ∈ s → abs (g n z) ≤ c * a ^ n := fun n z _ ↦ hf n
State after:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
⊢ Summable f

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
⊢ Summable f
Tactic:
have u := fast_series_converge_uniformly_on a0 a1 hg
State after:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : HasUniformSum (fun n z => g n z) (tsumOn fun n z => g n z) s
⊢ Summable f

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : HasUniformSum (fun n z => g n z) (tsumOn fun n z => g n z) s
⊢ Summable f
Tactic:
rw [HasUniformSum] at u
State after:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : TendstoUniformlyOn (fun N z => N.sum fun n => g n z) (tsumOn fun n z => g n z) atTop s
⊢ Summable f

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : TendstoUniformlyOn (fun N z => N.sum fun n => g n z) (tsumOn fun n z => g n z) atTop s
⊢ Summable f
Tactic:
rw [tendstoUniformlyOn_singleton_iff_tendsto] at u
State after:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : Filter.Tendsto (fun n => n.sum fun n => g n 0) atTop (𝓝 (tsumOn (fun n z => g n z) 0))
⊢ Summable f

State before:
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : Filter.Tendsto (fun n => n.sum fun n => g n 0) atTop (𝓝 (tsumOn (fun n z => g n z) 0))
⊢ Summable f
Tactic:
apply HasSum.summable
State after:
case h
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : Filter.Tendsto (fun n => n.sum fun n => g n 0) atTop (𝓝 (tsumOn (fun n z => g n z) 0))
⊢ HasSum f ?a

case a
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : Filter.Tendsto (fun n => n.sum fun n => g n 0) atTop (𝓝 (tsumOn (fun n z => g n z) 0))
⊢ ℂ

State before:
case h
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : Filter.Tendsto (fun n => n.sum fun n => g n 0) atTop (𝓝 (tsumOn (fun n z => g n z) 0))
⊢ HasSum f ?a

case a
f : ℕ → ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), Complex.abs (f n) ≤ c * a ^ n
s : Set ℂ := {0}
g : ℕ → ℂ → ℂ := fun n x => f n
hg : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (g n z) ≤ c * a ^ n
u : Filter.Tendsto (fun n => n.sum fun n => g n 0) atTop (𝓝 (tsumOn (fun n z => g n z) 0))
⊢ ℂ
Tactic:
assumption
State after:
no goals