positivity
case hp
n : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x✝ : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x✝.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x✝.log)) volume
x : ℝ
⊢ 0 x ≤ (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) x
no goals