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

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ UniformCauchySeqOn (fun N z => N.sum fun n => f n z) atTop s
Tactic:
rw [Metric.uniformCauchySeqOn_iff]
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < ε

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < ε
Tactic:
intro e ep
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e
Tactic:
rcases h e ep with ⟨m, hm⟩
State after:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e

State before:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e
Tactic:
use Finset.range m
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∀ m_1 ≥ Finset.range m, ∀ n ≥ Finset.range m, ∀ x ∈ s, dist (m_1.sum fun n => f n x) (n.sum fun n => f n x) < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∀ m_1 ≥ Finset.range m, ∀ n ≥ Finset.range m, ∀ x ∈ s, dist (m_1.sum fun n => f n x) (n.sum fun n => f n x) < e
Tactic:
intro A HA B HB z zs
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
HA : A ≥ Finset.range m
B : Finset ℕ
HB : B ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (A.sum fun n => f n z) (B.sum fun n => f n z) < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
HA : A ≥ Finset.range m
B : Finset ℕ
HB : B ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (A.sum fun n => f n z) (B.sum fun n => f n z) < e
Tactic:
calc dist (A.sum fun n ↦ f n z) (B.sum fun n ↦ f n z)
  _ ≤ (A ∆ B).sum fun n ↦ abs (f n z) := symmDiff_bound _ _ _
  _ < e := hm (A ∆ B) z (symmDiff_late HA HB) zs
State after:
no goals