exact (abs_nonneg _).trans this
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
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : |f 0| ≤ C
⊢ 0 ≤ C
no goals