internlm/Lean-Github huggingface dataset:
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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⟩
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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 _ _
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof 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
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ e / 4 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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]
Proof 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)
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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]
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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]
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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]
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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]
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof 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
Proof state after:
no goals
Theorem: CNonpos.degenerate
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
Tactic:
intro n z zs
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ s
⊢ f n z = 0
Theorem: CNonpos.degenerate
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ s
⊢ f n z = 0
Tactic:
specialize hf n z zs
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
⊢ f n z = 0
Theorem: CNonpos.degenerate
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
⊢ f n z = 0
Tactic:
have ca : c * a ^ n ≤ 0 := mul_nonpos_iff.mpr (Or.inr ⟨c0, by bound⟩)
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
ca : c * a ^ n ≤ 0
⊢ f n z = 0
Theorem: CNonpos.degenerate
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
ca : c * a ^ n ≤ 0
⊢ f n z = 0
Tactic:
exact Complex.abs.eq_zero.mp (le_antisymm (le_trans hf ca) (Complex.abs.nonneg _))
Proof state after:
no goals
Theorem: CNonpos.degenerate
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
⊢ 0 ≤ a ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: fast_series_converge_uniformly_on
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ HasUniformSum f (tsumOn f) s
Tactic:
by_cases c0 : c ≤ 0
Proof state after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
⊢ HasUniformSum f (tsumOn f) s

case neg
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : ¬c ≤ 0
⊢ HasUniformSum f (tsumOn f) s
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
⊢ HasUniformSum f (tsumOn f) s
Tactic:
have fz := CNonpos.degenerate c0 a0 hf
Proof state after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ HasUniformSum f (tsumOn f) s
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ HasUniformSum f (tsumOn f) s
Tactic:
rw [HasUniformSum, Metric.tendstoUniformlyOn_iff]
Proof state after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε
Tactic:
intro e ep
Proof state after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ (x : Finset ℕ), ∀ x_1 ∈ s, dist (tsumOn f x_1) (x.sum fun n => f n x_1) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ (x : Finset ℕ), ∀ x_1 ∈ s, dist (tsumOn f x_1) (x.sum fun n => f n x_1) < e
Tactic:
intro n z zs
Proof state after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (n.sum fun n => f n z) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (n.sum fun n => f n z) < e
Tactic:
rw [tsumOn]
Proof state after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (n.sum fun n => f n z) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (n.sum fun n => f n z) < e
Tactic:
simp_rw [fz _ z zs]
Proof state after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), 0) (n.sum fun n => 0) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), 0) (n.sum fun n => 0) < e
Tactic:
simp only [tsum_zero, Finset.sum_const_zero, dist_zero_left, Complex.norm_eq_abs,
  AbsoluteValue.map_zero]
Proof state after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ 0 < e