apply inv_le_one
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2))⁻¹ ≤ 1
case neg.ha
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 1 ≤ ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)