rw [smul_eq_mul, mul_assoc]
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun * ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2))