Theorem: cheby.bigO (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h : cheby f
l1 : 0 ≤ cumsum fun x => ‖f x‖
⊢ (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
Tactic:
obtain ⟨C, hC⟩ := h
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
Tactic:
apply isBigO_of_le' (c := C) atTop
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ ∀ (x : ℕ), ‖cumsum (fun x => ‖f x‖) x‖ ≤ C * ‖↑x‖

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ ∀ (x : ℕ), ‖cumsum (fun x => ‖f x‖) x‖ ≤ C * ‖↑x‖
Tactic:
intro n
State after:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ ‖cumsum (fun x => ‖f x‖) n‖ ≤ C * ‖↑n‖

State before:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ ‖cumsum (fun x => ‖f x‖) n‖ ≤ C * ‖↑n‖
Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr (l1 n)]
State after:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ cumsum (fun x => ‖f x‖) n ≤ C * ‖↑n‖

State before:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ cumsum (fun x => ‖f x‖) n ≤ C * ‖↑n‖
Tactic:
simpa using hC n
State after:
no goals