Theorem: WI_sum_Iab_le' (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
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
⊢ ∀ᶠ (x : ℝ) in atTop, (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
filter_upwards [eventually_gt_atTop (2 / b)] with x hx using WI_sum_Iab_le hpos hcheby hb hx
State after:
no goals