internlm/Lean-Github huggingface dataset:
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case h
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ f' t = (c' t * d t - c t * d' t) / d t ^ 2
Tactic:
rw [f'def, cdef, c'def, ddef, d'def]
Proof state after:
case h
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ (fun t =>
        (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) /
          (1 - (-(Complex.I * ↑t)).exp) ^ 2)
      t =
    ((fun t => -1) t * (fun t => 1 - (-(Complex.I * ↑t)).exp) t -
        (fun t => 1 - ↑t) t * (fun t => Complex.I * (-(Complex.I * ↑t)).exp) t) /
      (fun t => 1 - (-(Complex.I * ↑t)).exp) t ^ 2
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case h
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ (fun t =>
        (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) /
          (1 - (-(Complex.I * ↑t)).exp) ^ 2)
      t =
    ((fun t => -1) t * (fun t => 1 - (-(Complex.I * ↑t)).exp) t -
        (fun t => 1 - ↑t) t * (fun t => Complex.I * (-(Complex.I * ↑t)).exp) t) /
      (fun t => 1 - (-(Complex.I * ↑t)).exp) t ^ 2
Tactic:
simp
Proof state after:
case h
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2 =
    ((-(Complex.I * ↑t)).exp - 1 - (1 - ↑t) * (Complex.I * (-(Complex.I * ↑t)).exp)) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case h
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2 =
    ((-(Complex.I * ↑t)).exp - 1 - (1 - ↑t) * (Complex.I * (-(Complex.I * ↑t)).exp)) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
Tactic:
congr
Proof state after:
case h.e_a
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ -1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp =
    (-(Complex.I * ↑t)).exp - 1 - (1 - ↑t) * (Complex.I * (-(Complex.I * ↑t)).exp)
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case h.e_a
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
t✝ : ℝ
ht : t✝ ∈ Set.uIcc y' y
this : f = fun t => c t / d t
t : ℝ
⊢ -1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp =
    (-(Complex.I * ↑t)).exp - 1 - (1 - ↑t) * (Complex.I * (-(Complex.I * ↑t)).exp)
Tactic:
ring
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hc
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => c y) (c' t) t
Tactic:
rw [cdef, c'def]
Proof state after:
case hc
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => (fun t => 1 - ↑t) y) ((fun t => -1) t) t
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hc
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => (fun t => 1 - ↑t) y) ((fun t => -1) t) t
Tactic:
simp
Proof state after:
case hc
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => 1 - ↑y) (-1) t
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hc
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => 1 - ↑y) (-1) t
Tactic:
apply HasDerivAt.const_sub
Proof state after:
case hc.hf
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun x => ↑x) 1 t
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hc.hf
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun x => ↑x) 1 t
Tactic:
apply HasDerivAt.ofReal_comp
Proof state after:
case hc.hf.hf
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => y) 1 t
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hc.hf.hf
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => y) 1 t
Tactic:
apply hasDerivAt_id'
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hd
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => d y) (d' t) t
Tactic:
rw [ddef, d'def]
Proof state after:
case hd
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => (fun t => 1 - (-(Complex.I * ↑t)).exp) y) ((fun t => Complex.I * (-(Complex.I * ↑t)).exp) t) t
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hd
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => (fun t => 1 - (-(Complex.I * ↑t)).exp) y) ((fun t => Complex.I * (-(Complex.I * ↑t)).exp) t) t
Tactic:
simp
Proof state after:
case hd
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => 1 - (-(Complex.I * ↑y)).exp) (Complex.I * (-(Complex.I * ↑t)).exp) t
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hd
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => 1 - (-(Complex.I * ↑y)).exp) (Complex.I * (-(Complex.I * ↑t)).exp) t
Tactic:
rw [←neg_neg (Complex.I * Complex.exp (-(Complex.I * ↑t)))]
Proof state after:
case hd
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
t : ℝ
ht : t ∈ Set.uIcc y' y
this✝ : f = fun t => c t / d t
this : f' = fun t => (c' t * d t - c t * d' t) / d t ^ 2
⊢ HasDerivAt (fun y => 1 - (-(Complex.I * ↑y)).exp) (- -(Complex.I * (-(Complex.I * ↑t)).exp)) t