Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
f : ℝ → ℂ := fun t => (1 - ↑t) / (1 - (-(Complex.I * ↑t)).exp)
f' : ℝ → ℂ :=
  fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
f'def :
  f' = fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
c : ℝ → ℂ := fun t => 1 - ↑t
cdef : c = fun t => 1 - ↑t
c' : ℝ → ℂ := fun t => -1
c'def : c' = fun t => -1
d : ℝ → ℂ := fun t => 1 - (-(Complex.I * ↑t)).exp
ddef : d = fun t => 1 - (-(Complex.I * ↑t)).exp
d' : ℝ → ℂ := fun t => Complex.I * (-(Complex.I * ↑t)).exp
d'def : d' = fun t => Complex.I * (-(Complex.I * ↑t)).exp
d_nonzero : ∀ {t : ℝ}, t ∈ Set.uIcc y' y → d t ≠ 0
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
f'_cont : ContinuousOn (fun t => f' t) (Set.uIcc y' y)
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
calc ‖(1 - ↑y) / (1 - Complex.exp (-(Complex.I * ↑y))) - (1 - ↑y') / (1 - Complex.exp (-(Complex.I * ↑y')))‖
  _ = ‖f y - f y'‖ := by simp
  _ = ‖∫ (t : ℝ) in y'..y, f' t‖ := by
    congr 1
    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt]
    . exact f_deriv
    . apply f'_cont.intervalIntegrable
  _ = ‖∫ (t : ℝ) in Ι y' y, f' t‖ := by
    apply intervalIntegral.norm_intervalIntegral_eq
  _ ≤ ∫ (t : ℝ) in Ι y' y, ‖f' t‖ := by
    apply MeasureTheory.norm_integral_le_integral_norm
  _ ≤ ∫ (t : ℝ) in Ι y' y, 3 / ((y / 2) / 2) ^ 2 := by
    apply MeasureTheory.setIntegral_mono_on
    . apply f'_cont.norm.integrableOn_uIcc.mono_set
      apply Set.Ioc_subset_Icc_self
    . apply MeasureTheory.integrableOn_const.mpr
      right
      rw [Real.volume_uIoc]
      apply ENNReal.ofReal_lt_top
    . apply 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, Complex.norm_eq_abs, norm_pow]
      gcongr
      . calc Complex.abs (-1 + Complex.exp (-(Complex.I * ↑t)) + Complex.I * (↑t - 1) * Complex.exp (-(Complex.I * ↑t)))
          _ ≤ Complex.abs (-1 + Complex.exp (-(Complex.I * ↑t))) + Complex.abs (Complex.I * (↑t - 1) * Complex.exp (-(Complex.I * ↑t))) := by
            apply Complex.abs.isAbsoluteValue.abv_add
          _ ≤ Complex.abs (-1) + Complex.abs (Complex.exp (-(Complex.I * ↑t))) + Complex.abs (Complex.I * (↑t - 1) * Complex.exp (-(Complex.I * ↑t))) := by
            gcongr
            apply Complex.abs.isAbsoluteValue.abv_add
          _ ≤ 1 + 1 + 1 := by
            gcongr
            . simp
            . rw [mul_comm, ←neg_mul]
              norm_cast
              apply le_of_eq
              apply Complex.abs_exp_ofReal_mul_I
            . simp
              apply mul_le_one
              norm_cast
              rw [abs_of_nonpos] <;> linarith
              simp
              rw [mul_comm, ←neg_mul]
              norm_cast
              apply le_of_eq
              apply Complex.abs_exp_ofReal_mul_I
          _ = 3 := by norm_num
      . rw [mul_comm, ←neg_mul, mul_comm]
        norm_cast
        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]
  _ = (MeasureTheory.volume (Ι y' y)).toReal * (3 / ((y / 2) / 2) ^ 2) := by
    apply MeasureTheory.setIntegral_const
  _ = |y - y'| * (3 / ((y / 2) / 2) ^ 2) := by
    congr
    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
Proof state after:
no goals