Hilbert_kernel_bound

lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by  by_cases! h : 0 < |x - y| ∧ |x - y| < 1  · calc ‖K x y‖      _ ≤ 1 / ‖1 - exp (I * ↑(x - y))‖ := by        rw [K, k, norm_div]        gcongr        rw [norm_real, Real.norm_eq_abs, _root_.abs_of_nonneg]        · apply max_le _ zero_le_one; linarith [abs_nonneg (x-y)]        · exact le_max_right _ _      _ ≤ 1 / (|x - y| / 2) := by        gcongr        · linarith        · apply lower_secant_bound _ (by rfl)          rw [Set.mem_Icc]          constructor          · simp only [neg_mul, neg_add_le_iff_le_add]            calc |x - y|              _ ≤ 1 := h.2.le              _ ≤ 2 * π - 1 := by rw [le_sub_iff_add_le]; linarith [Real.two_le_pi]              _ ≤ 2 * π + (x - y) := by                rw [sub_eq_add_neg]                gcongr                exact (abs_le.mp h.2.le).1          · calc x - y              _ ≤ |x - y| := le_abs_self (x - y)              _ ≤ 1 := h.2.le              _ ≤ 2 * π - 1 := by rw [le_sub_iff_add_le]; linarith [Real.two_le_pi]              _ ≤ 2 * π - |x - y| := by gcongr; exact h.2.le      _ = 2 / |x - y| := by rw [one_div, inv_div]      _ ≤ (2 : ℝ) ^ (2 : ℝ) / (2 * |x - y|) := by ring_nf; trivial  · have : ‖K x y‖ = 0 := by      rw [norm_eq_zero, K, k, _root_.div_eq_zero_iff]      by_cases xeqy : x = y      · simp [xeqy]      · left        rw [ofReal_eq_zero, max_eq_right_iff, tsub_le_iff_right, zero_add]        exact h (abs_pos.mpr (sub_ne_zero.mpr xeqy))    rw [this]    exact div_nonneg (by norm_num) (by linarith [abs_nonneg (x-y)])