Theorem: crude_upper_bound (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
ψ : CS 2 ℂ
hψpos : ∀ (y : ℝ), 0 ≤ (𝓕 ψ.toFun y).re ∧ (𝓕 ψ.toFun y).im = 0
⊢ ∃ B, ∀ (x : ℝ), 0 < x → ‖∑' (n : ℕ), ↑(f n) / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ B
Tactic:
sorry
State after:
no goals