internlm/Lean-Github huggingface dataset:
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
⊢ |(-y')| ≤ 1

y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y)| ≤ 1
Tactic:
. rw [abs_neg, abs_of_nonneg yy'nonneg.2]
  assumption
Proof state after:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y)| ≤ 1
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
⊢ |(-y)| ≤ 1
Tactic:
. rw [abs_neg, abs_of_nonneg yy'nonneg.1]
  assumption
Proof state after:
no goals
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
⊢ ‖(1 - ↑|(-y)|) / (1 - (Complex.I * ↑(-y)).exp) - (1 - ↑|(-y')|) / (1 - (Complex.I * ↑(-y')).exp)‖ ≤
    2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
simp only [abs_neg, Complex.ofReal_neg, mul_neg, ge_iff_le]
Proof state after:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖(1 - ↑|y|) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑|y'|) / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)
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
⊢ ‖(1 - ↑|y|) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑|y'|) / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [abs_of_nonneg yy'nonneg.1, abs_of_nonneg yy'nonneg.2]
Proof state after:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
let f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - Complex.exp (-(Complex.I * t)))
Proof state after:
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)
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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)
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
set f' : ℝ → ℂ := fun t ↦ (-1 + Complex.exp (-(Complex.I * t)) + Complex.I * (t - 1) * Complex.exp (-(Complex.I * t))) / (1 - Complex.exp (-(Complex.I * t))) ^ 2 with f'def
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
set c : ℝ → ℂ := fun t ↦ (1 - t) with cdef
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
set c' : ℝ → ℂ := fun t ↦ -1 with c'def
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
set d : ℝ → ℂ := fun t ↦ (1 - Complex.exp (-(Complex.I * t))) with ddef
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
set d' : ℝ → ℂ := fun t ↦ Complex.I * Complex.exp (-(Complex.I * t)) with d'def
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
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
  rw [←norm_eq_zero]
  apply ne_of_gt
  calc ‖1 - Complex.exp (-(Complex.I * ↑t))‖
    _ ≥ |(1 - Complex.exp (-(Complex.I * ↑t))).im| := by
      simp only [Complex.norm_eq_abs, ge_iff_le]
      apply Complex.abs_im_le_abs
    _ = Real.sin t := by
      simp
      rw [Complex.exp_im]
      simp
      apply Real.sin_nonneg_of_nonneg_of_le_pi
      . linarith
      . linarith [Real.two_le_pi]
    _ > 0 := by
      apply Real.sin_pos_of_pos_of_lt_pi
      . linarith
      . linarith [Real.two_le_pi]
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
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 := by simp
  rw [this]
  have : f' = fun t ↦ ((c' t * d t - c t * d' t) / d t ^ 2) := by
    ext t
    rw [f'def, cdef, c'def, ddef, d'def]
    simp
    congr
    ring
  rw [this]
  apply HasDerivAt.div
  . rw [cdef, c'def]
    simp
    apply HasDerivAt.const_sub
    apply HasDerivAt.ofReal_comp
    apply hasDerivAt_id'
  . rw [ddef, d'def]
    simp
    rw [←neg_neg (Complex.I * Complex.exp (-(Complex.I * ↑t)))]
    apply HasDerivAt.const_sub
    rw [←neg_mul, mul_comm]
    apply HasDerivAt.cexp
    apply HasDerivAt.neg
    conv in fun (x : ℝ) ↦ Complex.I * (x : ℝ) =>
      ext
      rw [mul_comm]
    set e : ℂ → ℂ := fun t ↦ t * Complex.I with edef
    have : (fun (t : ℝ) ↦ t * Complex.I) = fun (t : ℝ) ↦ e t := by
      rw [edef]
    rw [this]
    apply HasDerivAt.comp_ofReal
    rw [edef]
    apply hasDerivAt_mul_const
  . exact d_nonzero ht
Proof state after:
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
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
⊢ ‖(1 - ↑y) / (1 - (-(Complex.I * ↑y)).exp) - (1 - ↑y') / (1 - (-(Complex.I * ↑y')).exp)‖ ≤
    2 ^ 6 * (1 / y) * (|y - y'| / y)
Tactic:
have f'_cont : ContinuousOn (fun t ↦ f' t) (Set.uIcc y' y) := by
  apply ContinuousOn.div
  . apply Continuous.continuousOn
    continuity
  . 
    apply Continuous.continuousOn
    apply Continuous.pow
    apply Continuous.sub
    . apply continuous_const
    . apply Continuous.cexp
      apply Continuous.neg
      apply Continuous.mul
      . apply continuous_const
      . apply Complex.continuous_ofReal
  . intro t ht
    simp
    apply d_nonzero ht
Proof state after:
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)
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
t : ℝ
ht : t ∈ Set.uIcc y' y
⊢ d t ≠ 0
Tactic:
rw [Set.mem_uIcc] at ht
Proof state after:
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
t : ℝ
ht : y' ≤ t ∧ t ≤ y ∨ y ≤ t ∧ t ≤ y'
⊢ d t ≠ 0
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
t : ℝ
ht : y' ≤ t ∧ t ≤ y ∨ y ≤ t ∧ t ≤ y'
⊢ d t ≠ 0
Tactic:
have ht' : 0 < t ∧ t ≤ 1 := by
  rcases ht with ht | ht <;> (constructor <;> linarith)
Proof state after:
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
t : ℝ
ht : y' ≤ t ∧ t ≤ y ∨ y ≤ t ∧ t ≤ y'
ht' : 0 < t ∧ t ≤ 1
⊢ d t ≠ 0
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
t : ℝ
ht : y' ≤ t ∧ t ≤ y ∨ y ≤ t ∧ t ≤ y'
ht' : 0 < t ∧ t ≤ 1
⊢ d t ≠ 0
Tactic:
rw [ddef]
Proof state after:
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
t : ℝ
ht : y' ≤ t ∧ t ≤ y ∨ y ≤ t ∧ t ≤ y'
ht' : 0 < t ∧ t ≤ 1
⊢ (fun t => 1 - (-(Complex.I * ↑t)).exp) t ≠ 0