Hilbert_kernel_regularity_main_part

lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ 0 ≤ y') (ypos : 0 < y)    (y2ley' : y / 2 ≤ y') (hy : y ≤ 1) (hy' : y' ≤ 1) :    ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by  rw [k_of_abs_le_one, k_of_abs_le_one]  · simp only [abs_neg, ofReal_neg, mul_neg]    rw [_root_.abs_of_nonneg yy'nonneg.1, _root_.abs_of_nonneg yy'nonneg.2]    set f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - exp (-(I * t))) with hf    set f' : ℝ → ℂ := fun t ↦ (-1 + exp (-(I * t)) + I * (t - 1) * exp (-(I * t)))      / (1 - exp (-(I * t))) ^ 2 with f'def    set c : ℝ → ℂ := fun t ↦ (1 - t) with cdef    set c' : ℝ → ℂ := fun t ↦ -1 with c'def    set d : ℝ → ℂ := fun t ↦ (1 - exp (-(I * t))) with ddef    set d' : ℝ → ℂ := fun t ↦ I * exp (-(I * t)) with d'def    have d_nonzero {t : ℝ} (ht : t ∈ Set.uIcc y' y) : d t ≠ 0 := by      rw [Set.mem_uIcc] at ht      have ht' : 0 < t ∧ t ≤ 1 := by        rcases ht with ht | ht <;> (constructor <;> linarith)      rw [ddef]      simp only [ne_eq]      rw [←norm_eq_zero]      apply ne_of_gt      calc ‖1 - exp (-(I * ↑t))‖        _ ≥ |(1 - exp (-(I * ↑t))).im| := by          simp only [ge_iff_le]          apply abs_im_le_norm        _ = Real.sin t := by          simp only [sub_im, one_im, exp_im, neg_re, mul_re,            I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero,            sub_self, neg_zero, Real.exp_zero, neg_im, mul_im, one_mul, zero_add,            Real.sin_neg, mul_neg, sub_neg_eq_add, abs_eq_self]          exact Real.sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith [Real.two_le_pi])        _ > 0 := Real.sin_pos_of_pos_of_lt_pi (by linarith) (by linarith [Real.two_le_pi])    have f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t := by      intro t ht      have : f = fun t ↦ c t / d t := rfl      rw [this]      have : f' = fun t ↦ ((c' t * d t - c t * d' t) / d t ^ 2) := by ext t; ring      rw [this]      apply HasDerivAt.div _ _ _      · exact cdef ▸ c'def ▸ HasDerivAt.const_sub _ (HasDerivAt.ofReal_comp (hasDerivAt_id' _))      · rw [ddef, d'def]        simp only        rw [←neg_neg (I * exp (-(I * ↑t)))]        rw [←neg_mul, mul_comm]        apply HasDerivAt.const_sub _ (HasDerivAt.cexp (HasDerivAt.neg _))        conv in fun (x : ℝ) ↦ I * (x : ℝ) => ext; rw [mul_comm]        set e : ℂ → ℂ := fun t ↦ t * I with edef        have : (fun (t : ℝ) ↦ t * I) = fun (t : ℝ) ↦ e t := by rw [edef]        rw [this]        apply HasDerivAt.comp_ofReal        rw [edef]        apply hasDerivAt_mul_const      · exact d_nonzero ht    have f'_cont : ContinuousOn (fun t ↦ f' t) (Set.uIcc y' y) :=      ContinuousOn.div (by fun_prop) (by fun_prop) (by simpa using fun _ ht ↦ d_nonzero ht)    calc ‖(1 - ↑y) / (1 - exp (-(I * ↑y))) - (1 - ↑y') / (1 - exp (-(I * ↑y')))‖      _ = ‖f y - f y'‖ := by simp [hf]      _ = ‖∫ (t : ℝ) in y'..y, f' t‖ := by        congr 1        rw [intervalIntegral.integral_eq_sub_of_hasDerivAt]        · exact f_deriv        · exact f'_cont.intervalIntegrable      _ = ‖∫ (t : ℝ) in Ι y' y, f' t‖ := intervalIntegral.norm_intervalIntegral_eq _ _ _ _      _ ≤ ∫ (t : ℝ) in Ι y' y, ‖f' t‖ := norm_integral_le_integral_norm _      _ ≤ ∫ (t : ℝ) in Ι y' y, 3 / ((y / 2) / 2) ^ 2 := by        apply setIntegral_mono_on        · exact f'_cont.norm.integrableOn_uIcc.mono_set Set.Ioc_subset_Icc_self        · apply (integrableOn_const_iff).mpr          rw [Real.volume_uIoc]          right          exact ENNReal.ofReal_lt_top        · exact measurableSet_uIoc        · intro t ht          rw [Set.mem_uIoc] at ht          have ht' : 0 < t ∧ t ≤ 1 := by            rcases ht with ht | ht <;> (constructor <;> linarith)          rw [f'def]          simp only [norm_div, norm_pow]          gcongr          · calc ‖(-1 + exp (-(I * ↑t)) +              I * (↑t - 1) * exp (-(I * ↑t)))‖              _ ≤ ‖(-1 + exp (-(I * ↑t)))‖ +                ‖(I * (↑t - 1) * exp (-(I * ↑t)))‖ :=                  norm_add_le ..              _ ≤ ‖(-1 : ℂ)‖ + ‖(exp (-(I * ↑t)))‖ +                ‖(I * (↑t - 1) * exp (-(I * ↑t)))‖ := by                gcongr                exact norm_add_le ..              _ ≤ 1 + 1 + 1 := by                gcongr                · simp                · rw [mul_comm, ←neg_mul]                  norm_cast                  exact le_of_eq (norm_exp_ofReal_mul_I _)                · simp only [Complex.norm_mul, norm_I, one_mul]                  apply mul_le_one₀                  on_goal 1 => norm_cast                  rw [Real.norm_of_nonpos] <;> linarith                  · exact norm_nonneg _                  rw [mul_comm, ←neg_mul]                  norm_cast                  exact le_of_eq (norm_exp_ofReal_mul_I _)              _ = 3 := by norm_num          · rw_mod_cast [mul_comm, ←neg_mul, mul_comm]            apply lower_secant_bound            · simp only [neg_mul, Set.mem_Icc, neg_add_le_iff_le_add, le_add_neg_iff_add_le,              neg_le_sub_iff_le_add]              constructor <;> linarith [Real.two_le_pi, Real.two_pi_pos]            · rw [abs_neg, le_abs]              left              rcases ht with ht | ht <;> linarith [ht.1]      _ = (volume (Ι y' y)).toReal * (3 / ((y / 2) / 2) ^ 2) :=        setIntegral_const _      _ = |y - y'| * (3 / ((y / 2) / 2) ^ 2) := by        rw [Real.volume_uIoc, ENNReal.toReal_ofReal (abs_nonneg (y - y'))]      _ = (3 * (2 * 2) ^ 2) * (1 / y) * (|y - y'| / y) := by ring      _ ≤ 2 ^ 6 * (1 / y) * (|y - y'| / y) := by gcongr; norm_num  · rwa [abs_neg, _root_.abs_of_nonneg yy'nonneg.2]  · rwa [abs_neg, _root_.abs_of_nonneg yy'nonneg.1]