simp [W21.norm]
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (W21.norm ψ.toFun * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
      (Complex.abs (f i) / ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹) =
    Complex.abs (f i) / ↑i *
      (((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
        (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹)