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

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ HasUniformSum f (tsumOn f) s
Tactic:
rw [HasUniformSum, Metric.tendstoUniformlyOn_iff]
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f 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 : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Tactic:
rcases h (e / 4) (by linarith) 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 / 4
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f 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 / 4
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Tactic:
rw [Filter.eventually_atTop]
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 / 4
⊢ ∃ a, ∀ b ≥ a, ∀ x ∈ s, dist (tsumOn f x) (b.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 / 4
⊢ ∃ a, ∀ b ≥ a, ∀ x ∈ s, dist (tsumOn f x) (b.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 / 4
⊢ ∀ b ≥ Finset.range m, ∀ x ∈ s, dist (tsumOn f x) (b.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 / 4
⊢ ∀ b ≥ Finset.range m, ∀ x ∈ s, dist (tsumOn f x) (b.sum fun n => f n x) < e
Tactic:
intro N Nm 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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (N.sum fun n => f n z) < e
Tactic:
rw [tsumOn]
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (N.sum fun n => f n z) < e
Tactic:
generalize G : tsum (fun n ↦ f n z) = g
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
⊢ dist g (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
have S : Summable (fun n ↦ f n z) := uniformVanishing_to_summable zs h
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
⊢ dist g (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
have GS : HasSum (fun n ↦ f n z) g := by rw [← G]; exact Summable.hasSum S
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
GS : HasSum (fun n => f n z) g
⊢ dist g (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
GS : HasSum (fun n => f n z) g
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
clear S
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : HasSum (fun n => f n z) g
⊢ dist g (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : HasSum (fun n => f n z) g
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
rw [HasSum] at GS
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : Filter.Tendsto (fun s => s.sum fun b => f b z) atTop (𝓝 g)
⊢ dist g (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : Filter.Tendsto (fun s => s.sum fun b => f b z) atTop (𝓝 g)
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
rw [Metric.tendsto_atTop] at GS
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => f b z) g < ε
⊢ dist g (N.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => f b z) g < ε
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
rcases GS (e / 4) (by linarith) with ⟨M, HM⟩
State after:
case h.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => f b z) g < ε
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => f b z) g < ε
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
clear GS G h
State after:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
set A := N ∪ M \ N
State after:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
A : Finset ℕ := N ∪ M \ N
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
A : Finset ℕ := N ∪ M \ N
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
have AM : M ⊆ A := subset_union_sdiff _ _
State after:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
HM : ∀ n ≥ M, dist (n.sum fun b => f b z) g < e / 4
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
simp at HM
State after:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : ∀ (n : Finset ℕ), M ⊆ n → dist (n.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : ∀ (n : Finset ℕ), M ⊆ n → dist (n.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
specialize HM A AM
State after:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist (A.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist (A.sum fun b => f b z) g < e / 4
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
rw [dist_comm] at HM
State after:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ dist g (N.sum fun n => f n z) < e

State before:
case h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
calc dist g (N.sum fun n ↦ f n z)
  _ ≤ dist g (A.sum fun n ↦ f n z) + dist (A.sum fun n ↦ f n z) (N.sum fun n ↦ f n z) := by bound
  _ ≤ e / 4 + dist (A.sum fun n ↦ f n z) (N.sum fun n ↦ f n z) := by linarith
  _ = e / 4 + dist ((N.sum fun n ↦ f n z) + (M \ N).sum fun n ↦ f n z)
      (N.sum fun n ↦ f n z) := by rw [Finset.sum_union Finset.disjoint_sdiff]
  _ = e / 4 + abs (((N.sum fun n ↦ f n z) + (M \ N).sum fun n ↦ f n z) -
      N.sum fun n ↦ f n z) := by rw [Complex.dist_eq]
  _ = e / 4 + abs ((M \ N).sum fun n ↦ f n z) := by ring_nf
  _ ≤ e / 4 + (M \ N).sum fun n ↦ abs (f n z) := by
    linarith [finset_complex_abs_sum_le (M \ N) fun n ↦ f n z]
  _ ≤ e / 4 + e / 4 := by linarith [hm (M \ N) z (sdiff_late M Nm) zs]
  _ = e / 2 := by ring
  _ < e := by linarith
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ e / 4 > 0
Tactic:
linarith
State after:
no goals

State before:
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
⊢ HasSum (fun n => f n z) g
Tactic:
rw [← G]
State after:
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
⊢ HasSum (fun n => f n z) (∑' (n : ℕ), f n z)

State before:
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
⊢ HasSum (fun n => f n z) (∑' (n : ℕ), f n z)
Tactic:
exact Summable.hasSum S
State after:
no goals

State before:
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 / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
GS : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => f b z) g < ε
⊢ e / 4 > 0
Tactic:
linarith
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ dist g (N.sum fun n => f n z) ≤ dist g (A.sum fun n => f n z) + dist (A.sum fun n => f n z) (N.sum fun n => f n z)
Tactic:
bound
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ dist g (A.sum fun n => f n z) + dist (A.sum fun n => f n z) (N.sum fun n => f n z) ≤
    e / 4 + dist (A.sum fun n => f n z) (N.sum fun n => f n z)
Tactic:
linarith
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ e / 4 + dist (A.sum fun n => f n z) (N.sum fun n => f n z) =
    e / 4 + dist ((N.sum fun n => f n z) + (M \ N).sum fun n => f n z) (N.sum fun n => f n z)
Tactic:
rw [Finset.sum_union Finset.disjoint_sdiff]
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ e / 4 + dist ((N.sum fun n => f n z) + (M \ N).sum fun n => f n z) (N.sum fun n => f n z) =
    e / 4 + Complex.abs (((N.sum fun n => f n z) + (M \ N).sum fun n => f n z) - N.sum fun n => f n z)
Tactic:
rw [Complex.dist_eq]
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ e / 4 + Complex.abs (((N.sum fun n => f n z) + (M \ N).sum fun n => f n z) - N.sum fun n => f n z) =
    e / 4 + Complex.abs ((M \ N).sum fun n => f n z)
Tactic:
ring_nf
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ e / 4 + Complex.abs ((M \ N).sum fun n => f n z) ≤ e / 4 + (M \ N).sum fun n => Complex.abs (f n z)
Tactic:
linarith [finset_complex_abs_sum_le (M \ N) fun n ↦ f n z]
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ (e / 4 + (M \ N).sum fun n => Complex.abs (f n z)) ≤ e / 4 + e / 4
Tactic:
linarith [hm (M \ N) z (sdiff_late M Nm) zs]
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ e / 4 + e / 4 = e / 2
Tactic:
ring
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
M : Finset ℕ
A : Finset ℕ := N ∪ M \ N
AM : M ⊆ A
HM : dist g (A.sum fun b => f b z) < e / 4
⊢ e / 2 < e
Tactic:
linarith
State after:
no goals