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

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
⊢ Summable fun n => f n z
Tactic:
rw [summable_iff_vanishing_norm]
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < ε

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < ε
Tactic:
intro e ep
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e
Tactic:
rcases h e ep with ⟨m, hm⟩
State after:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e

State before:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e
Tactic:
use Finset.range m
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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
⊢ ∀ (t : Finset ℕ), Disjoint t (Finset.range m) → ‖t.sum fun i => f i z‖ < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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
⊢ ∀ (t : Finset ℕ), Disjoint t (Finset.range m) → ‖t.sum fun i => f i z‖ < e
Tactic:
intro A d
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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 ℕ
d : Disjoint A (Finset.range m)
⊢ ‖A.sum fun i => f i z‖ < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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 ℕ
d : Disjoint A (Finset.range m)
⊢ ‖A.sum fun i => f i z‖ < e
Tactic:
calc ‖A.sum (fun n ↦ f n z)‖
  _ ≤ A.sum (fun n ↦ ‖f n z‖) := by bound
  _ < e := hm _ _ (late_iff_disjoint_range.mpr d) zs
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
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 ℕ
d : Disjoint A (Finset.range m)
⊢ ‖A.sum fun n => f n z‖ ≤ A.sum fun n => ‖f n z‖
Tactic:
bound
State after:
no goals