niceKernel_lowerBound

lemma niceKernel_lowerBound {r x : ℝ} (hr : 0 < r) (h'r : r < 1) (hx : r ≤ x ∧ x ≤ π) :    1 + r / ‖1 - exp (I * x)‖ ^ 2 ≤ 5 * niceKernel r x := by  have : exp (I * x) ≠ 1 := by    simp only [ne_eq, exp_I_mul_eq_one_iff_of_lt_of_lt x (by linarith) (by linarith)]; linarith  simp only [niceKernel, this, ↓reduceIte, ge_iff_le]  rw [mul_min_of_nonneg _ _ (by norm_num)]  simp only [normSq_eq_norm_sq, le_inf_iff]  refine ⟨?_, le_mul_of_one_le_left (by positivity) (by norm_num)⟩  apply (niceKernel_upperBound_aux hr hx).trans  calc 1 + 4 * r / x ^ 2  _ ≤ r ⁻¹ + 4 * r / (r ^ 2) := by    gcongr    · apply le_inv_of_le_inv₀ hr (by simpa using h'r.le)    · exact hx.1  _ = 5 * r ⁻¹ := by field_simp; norm_num