Hilbert_kernel_regularity

lemma Hilbert_kernel_regularity {x y y' : ℝ} :    2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)  := by  rw [K, K]  wlog x_eq_zero : x = 0 generalizing x y y'  · intro h    set x_ := (0 : ℝ) with x_def    set y_ := y - x with y_def    set y'_ := y' - x with y'_def    have h_ : 2 * |y_ - y'_| ≤ |x_ - y_| := by simpa [x_def, y_def, y'_def]    have := this x_def h_    rw [x_def, y_def, y'_def] at this    simpa  rw [x_eq_zero]  intro h  simp only [zero_sub, abs_neg] at h  simp only [zero_sub, abs_neg]  wlog! yy'nonneg : 0 ≤ y ∧ 0 ≤ y' generalizing y y'  · by_cases! yge0 : 0 ≤ y    · exfalso      rw [_root_.abs_of_nonneg yge0, _root_.abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]    by_cases! y'ge0 : 0 ≤ y'    · exfalso      rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith    /- This is the only interesting case. -/    set! y_ := -y with y_def    set! y'_ := -y' with y'_def    have h_ : 2 * |y_ - y'_| ≤ |y_| := by      rw [y_def, y'_def, ← abs_neg]      simpa [neg_add_eq_sub]    have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith    have := this h_ y_y'_nonneg    rw [y_def, y'_def] at this    simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this    rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k,      ← abs_neg (y' - y)] at this    simpa  /-"Wlog" 0 < y-/  by_cases! ypos : y ≤ 0  · have y_eq_zero : y = 0 := le_antisymm ypos yy'nonneg.1    have y'_eq_zero : y' = 0 := by      simp [y_eq_zero, _root_.abs_of_nonneg yy'nonneg.2] at h      linarith    simp [y_eq_zero, y'_eq_zero]  /- Beginning of the main proof -/  have y2ley' : y / 2 ≤ y' := by    rw [div_le_iff₀ two_pos]    calc y      _ = 2 * (y - y') - y + 2 * y' := by ring      _ ≤ 2 * |y - y'| - y + 2 * y' := by gcongr; exact le_abs_self _      _ ≤ y - y + 2 * y' := by        gcongr        rw [abs_eq_self.mpr yy'nonneg.1] at h        exact h      _ = y' * 2 := by ring  /- Distinguish four cases -/  rcases le_or_gt y 1, le_or_gt y' 1 with ⟨hy | hy, hy' | hy'⟩  · apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy')    gcongr <;> norm_num  · rw [@k_of_one_le_abs (-y')]    · calc ‖k (-y) - 0‖        _ = ‖k (-y) - k (-1)‖ := by          congr          apply (k_of_one_le_abs _).symm          simp        _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by          apply Hilbert_kernel_regularity_main_part          constructor          all_goals linarith        _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by          gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)          rw [abs_sub_comm, _root_.abs_of_nonneg, abs_sub_comm, _root_.abs_of_nonneg] <;> linarith        _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by          gcongr <;> norm_num    · rw [abs_neg, _root_.abs_of_nonneg] <;> linarith  · rw [@k_of_one_le_abs (-y)]    · calc ‖0 - k (-y')‖        _ = ‖k (-1) - k (-y')‖ := by          congr          apply (k_of_one_le_abs _).symm          simp only [abs_neg, abs_one, le_refl]        _ = ‖k (-y') - k (-1)‖ := by rw [norm_sub_rev]        _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by          apply Hilbert_kernel_regularity_main_part          constructor          all_goals linarith        _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by          congr          · simp [_root_.abs_of_nonneg, yy'nonneg.2]          · rw [abs_of_nonpos, neg_sub]            linarith          · simp [_root_.abs_of_nonneg, yy'nonneg.2]        _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by          gcongr          apply div_nonneg <;> linarith        _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by          ring        _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by          gcongr          on_goal 2 => rw [_root_.abs_of_nonneg] <;> linarith          all_goals rw [_root_.abs_of_nonneg yy'nonneg.1]        _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by norm_num    · rw [abs_neg, _root_.abs_of_nonneg] <;> linarith  · calc ‖k (-y) - k (-y')‖      _ = 0 := by        rw [norm_sub_eq_zero_iff, k_of_one_le_abs,          k_of_one_le_abs] <;> (rw [abs_neg, _root_.abs_of_nonneg] <;> linarith)      _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := mul_nonneg (mul_nonneg (by norm_num) (by simp))        (mul_nonneg (by norm_num) (by simp))