Theorem: summable_iff_bounded' (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
obtain ⟨N, hu⟩ := eventually_atTop.mp hu
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
have e2 : cumsum (fun i ↦ u (i + N)) = fun n => cumsum u (n + N) - cumsum u N := by
  ext n ; simp_rw [cumsum, add_comm _ N, Finset.sum_range_add] ; ring
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
rw [← summable_nat_add_iff N, summable_iff_bounded (fun n => hu _ <| Nat.le_add_left N n), e2]
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ (atTop.BoundedAtFilter fun n => cumsum u (n + N) - cumsum u N) ↔ atTop.BoundedAtFilter (cumsum u)

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ (atTop.BoundedAtFilter fun n => cumsum u (n + N) - cumsum u N) ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
simp_rw [sub_eq_add_neg, BoundedAtFilter.add_const, BoundedAtFilter.comp_add]
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
⊢ (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
Tactic:
ext n
State after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ cumsum (fun i => u (i + N)) n = cumsum u (n + N) - cumsum u N

State before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ cumsum (fun i => u (i + N)) n = cumsum u (n + N) - cumsum u N
Tactic:
simp_rw [cumsum, add_comm _ N, Finset.sum_range_add]
State after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ ∑ x ∈ Finset.range n, u (N + x) =
    ∑ x ∈ Finset.range N, u x + ∑ x ∈ Finset.range n, u (N + x) - ∑ x ∈ Finset.range N, u x

State before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ ∑ x ∈ Finset.range n, u (N + x) =
    ∑ x ∈ Finset.range N, u x + ∑ x ∈ Finset.range n, u (N + x) - ∑ x ∈ Finset.range N, u x
Tactic:
ring
State after:
no goals