gg_le_one

lemma gg_le_one (i : ℕ) : gg x i ≤ 1 := by  by_cases hi : i = 0 <;> simp only [gg, hi, CharP.cast_eq_zero, div_zero, one_div, mul_inv_rev,    zero_div, Real.log_zero, mul_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,    add_zero, inv_one, mul_one, zero_le_one]  have l1 : 1 ≤ (i : ℝ) := by simp ; omega  have l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * Real.log (↑i / x)) ^ 2 := by    simp only [le_add_iff_nonneg_right] ; positivity  rw [← mul_inv] ; apply inv_le_one_of_one_le₀ ; simpa using mul_le_mul l1 l2 zero_le_one (by simp)