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 : 0 ≤ u
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
have l1 : (cumsum u =O[atTop] 1) ↔ _ := isBigO_one_nat_atTop_iff
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
have l2 n : ‖cumsum u n‖ = cumsum u n := by simpa using cumsum_nonneg hu n
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
simp only [BoundedAtFilter, l1, l2]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C
Tactic:
constructor <;> intro ⟨C, h1⟩
State after:
case mp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : HasSum u C
⊢ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C

case mpr
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : ∀ (n : ℕ), cumsum u n ≤ C
⊢ Summable u

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
n : ℕ
⊢ ‖cumsum u n‖ = cumsum u n
Tactic:
simpa using cumsum_nonneg hu n
State after:
no goals

State before:
case mp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : HasSum u C
⊢ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C
Tactic:
exact ⟨C, fun n => sum_le_hasSum _ (fun i _ => hu i) h1⟩
State after:
no goals

State before:
case mpr
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : ∀ (n : ℕ), cumsum u n ≤ C
⊢ Summable u
Tactic:
exact summable_of_sum_range_le hu h1
State after:
no goals