simp [abs_eq_self.mpr hC, abs_eq_self.mpr pi_nonneg, abs_eq_self.mpr this]
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)‖ ≤ C * ‖1 n‖
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2) ≤ C