internlm/Lean-Github huggingface dataset:
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
⊢ 0 < e
Tactic:
assumption
Proof state after:
no goals
Theorem: fast_series_converge_uniformly_on
Proof state before:
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
Tactic:
simp only [not_le] at c0
Proof state after:
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 : 0 < c
⊢ HasUniformSum f (tsumOn f) s
Theorem: fast_series_converge_uniformly_on
Proof state before:
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 : 0 < c
⊢ HasUniformSum f (tsumOn f) s
Tactic:
apply uniformVanishing_to_tendsto_uniformly_on
Proof state after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
⊢ UniformVanishing f s
Theorem: fast_series_converge_uniformly_on
Proof state before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
⊢ UniformVanishing f s
Tactic:
intro e ep
Proof state after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
set t := (1 - ↑a) / ↑c * (e / 2)
Proof state after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
have tp : t > 0 := by bound
Proof state after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
rcases exists_pow_lt_of_lt_one tp a1 with ⟨n, nt⟩
Proof state after:
case neg.h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case neg.h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
use n
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
intro N z NL zs
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
⊢ (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
⊢ (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
have a1p : 1 - (a : ℝ) > 0 := by linarith
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (N.sum fun n => Complex.abs (f n z)) < e
Theorem: fast_series_converge_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
calc (N.sum fun n ↦ abs (f n z))
  _ ≤ N.sum fun n ↦ c * a ^ n := Finset.sum_le_sum fun n _ ↦ hf n z zs
  _ = c * N.sum fun n ↦ a ^ n := (Finset.mul_sum _ _ _).symm
  _ ≤ c * (a ^ n * (1 - a)⁻¹) := by bound [late_geometric_bound NL a0 a1]
  _ = a ^ n * (c * (1 - a)⁻¹) := by ring
  _ ≤ t * (c * (1 - a)⁻¹) := by bound
  _ = (1 - a) / c * (e / 2) * (c * (1 - a)⁻¹) := rfl
  _ = (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2) := by ring
  _ = 1 * 1 * (e / 2) := by rw [mul_inv_cancel a1p.ne', div_self c0.ne']
  _ = e / 2 := by ring
  _ < e := by linarith
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
⊢ t > 0
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
⊢ 1 - a > 0
Tactic:
linarith
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (c * N.sum fun n => a ^ n) ≤ c * (a ^ n * (1 - a)⁻¹)
Tactic:
bound [late_geometric_bound NL a0 a1]
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ c * (a ^ n * (1 - a)⁻¹) = a ^ n * (c * (1 - a)⁻¹)
Tactic:
ring
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ a ^ n * (c * (1 - a)⁻¹) ≤ t * (c * (1 - a)⁻¹)
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (1 - a) / c * (e / 2) * (c * (1 - a)⁻¹) = (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2)
Tactic:
ring
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2) = 1 * 1 * (e / 2)
Tactic:
rw [mul_inv_cancel a1p.ne', div_self c0.ne']
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ 1 * 1 * (e / 2) = e / 2
Tactic:
ring
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
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ e / 2 < e
Tactic:
linarith
Proof state after:
no goals
Theorem: fast_series_converge_at
Proof 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}
Proof 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
Theorem: fast_series_converge_at
Proof 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
Proof 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
Theorem: fast_series_converge_at
Proof 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
Proof 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
Theorem: fast_series_converge_at
Proof 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
Proof 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
Theorem: fast_series_converge_at
Proof 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
Proof 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
Theorem: fast_series_converge_at
Proof 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
Proof 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
Theorem: fast_series_converge_at
Proof 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
Proof 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))
⊢ ℂ
Theorem: fast_series_converge_at
Proof 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
Proof state after:
no goals
Theorem: fast_series_converge
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ ∃ g, AnalyticOn ℂ g s ∧ HasSumOn f g s
Tactic:
use tsumOn f
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s ∧ HasSumOn f (tsumOn f) s
Theorem: fast_series_converge
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s ∧ HasSumOn f (tsumOn f) s
Tactic:
constructor
Proof state after:
case h.left
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s

case h.right
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ HasSumOn f (tsumOn f) s
Theorem: fast_series_converge
Proof state before:
case h.left
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ AnalyticOn ℂ (tsumOn f) s
Tactic:
exact uniform_analytic_lim o (fun N ↦ N.analyticOn_sum fun _ _ ↦ h _)
  (fast_series_converge_uniformly_on a0 a1 hf)
Proof state after:
no goals
Theorem: fast_series_converge
Proof state before:
case h.right
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ HasSumOn f (tsumOn f) s
Tactic:
exact fun z zs ↦ Summable.hasSum (fast_series_converge_at a0 a1 fun n ↦ hf n z zs)
Proof state after:
no goals
Theorem: sum_cons
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : HasSum f g
⊢ HasSum (Stream'.cons a f) (a + g)
Tactic:
rw [HasSum] at h ⊢
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Theorem: sum_cons
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_add_left a) g) h
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Theorem: sum_cons
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
have s : ((fun z ↦ a + z) ∘ fun N : Finset ℕ ↦ N.sum f) =
    (fun N : Finset ℕ ↦ N.sum (Stream'.cons a f)) ∘ push := by
  apply funext; intro N; simp; exact push_sum
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Theorem: sum_cons
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
rw [s] at ha
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.sum (Stream'.cons a f)) ∘ push) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Theorem: sum_cons
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.sum (Stream'.cons a f)) ∘ push) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
exact tendsto_comp_push.mp ha
Proof state after:
no goals
Theorem: sum_cons
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
Tactic:
apply funext
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ ∀ (x : Finset ℕ), ((fun z => a + z) ∘ fun N => N.sum f) x = ((fun N => N.sum (Stream'.cons a f)) ∘ push) x
Theorem: sum_cons
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ ∀ (x : Finset ℕ), ((fun z => a + z) ∘ fun N => N.sum f) x = ((fun N => N.sum (Stream'.cons a f)) ∘ push) x
Tactic:
intro N
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ ((fun z => a + z) ∘ fun N => N.sum f) N = ((fun N => N.sum (Stream'.cons a f)) ∘ push) N
Theorem: sum_cons
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ ((fun z => a + z) ∘ fun N => N.sum f) N = ((fun N => N.sum (Stream'.cons a f)) ∘ push) N
Tactic:
simp
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ a + N.sum f = (push N).sum (Stream'.cons a f)
Theorem: sum_cons
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ a + N.sum f = (push N).sum (Stream'.cons a f)
Tactic:
exact push_sum
Proof state after:
no goals
Theorem: sum_cons'
Proof state before:
a : ℂ
f : ℕ → ℂ
h : Summable f
⊢ tsum (Stream'.cons a f) = a + tsum f
Tactic:
rcases h with ⟨g, h⟩
Proof state after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + tsum f
Theorem: sum_cons'
Proof state before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + tsum f
Tactic:
rw [HasSum.tsum_eq h]
Proof state after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + g
Theorem: sum_cons'
Proof state before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + g
Tactic:
rw [HasSum.tsum_eq _]
Proof state after:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ HasSum (fun b => Stream'.cons a f b) (a + g)
Theorem: sum_cons'
Proof state before:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ HasSum (fun b => Stream'.cons a f b) (a + g)
Tactic:
exact sum_cons h
Proof state after:
no goals
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
⊢ HasSum (fun n => f (n + 1)) (g - f 0)
Tactic:
have c := sum_cons (a := -f 0) h
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ HasSum (fun n => f (n + 1)) (g - f 0)