have l2 (i : ℕ) (_ : i ∈ Finset.range ⌈b * x⌉₊) : f i * indicator (Ico a b) 1 (i / x) ≤ |f i| := by
  rw [abs_eq_self.mpr (hpos _)]
  convert_to _ ≤ f i * 1 ; ring
  apply mul_le_mul_of_nonneg_left ?_ (hpos _)
  by_cases hi : (i / x) ∈ (Ico a b) <;> simp [hi]
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
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
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|
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b