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
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
e : ℂ → ℂ := fun t => t * Complex.I
edef : e = fun t => t * Complex.I
⊢ (fun t => ↑t * Complex.I) = fun t => e ↑t
Tactic:
rw [edef]
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hx
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
⊢ d t ≠ 0
Tactic:
exact d_nonzero ht
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg
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
⊢ ContinuousOn (fun t => (1 - (-(Complex.I * ↑t)).exp) ^ 2) (Set.uIcc y' y)

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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ ∀ x ∈ Set.uIcc y' y, (1 - (-(Complex.I * ↑x)).exp) ^ 2 ≠ 0
Tactic:
. 
  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
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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ ∀ x ∈ Set.uIcc y' y, (1 - (-(Complex.I * ↑x)).exp) ^ 2 ≠ 0
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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ ∀ x ∈ Set.uIcc y' y, (1 - (-(Complex.I * ↑x)).exp) ^ 2 ≠ 0
Tactic:
. intro t ht
  simp
  apply d_nonzero ht
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case 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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ ContinuousOn (fun t => -1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) (Set.uIcc y' y)
Tactic:
apply Continuous.continuousOn
Proof state after:
case hf.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun t => -1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hf.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun t => -1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp
Tactic:
continuity
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg
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
⊢ ContinuousOn (fun t => (1 - (-(Complex.I * ↑t)).exp) ^ 2) (Set.uIcc y' y)
Tactic:
apply Continuous.continuousOn
Proof state after:
case hg.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun t => (1 - (-(Complex.I * ↑t)).exp) ^ 2
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun t => (1 - (-(Complex.I * ↑t)).exp) ^ 2
Tactic:
apply Continuous.pow
Proof state after:
case hg.h.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun b => 1 - (-(Complex.I * ↑b)).exp
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg.h.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun b => 1 - (-(Complex.I * ↑b)).exp
Tactic:
apply Continuous.sub
Proof state after:
case hg.h.h.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun x => 1

case hg.h.h.hg
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
⊢ Continuous fun x => (-(Complex.I * ↑x)).exp
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg.h.h.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun x => 1

case hg.h.h.hg
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
⊢ Continuous fun x => (-(Complex.I * ↑x)).exp
Tactic:
. apply continuous_const
Proof state after:
case hg.h.h.hg
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
⊢ Continuous fun x => (-(Complex.I * ↑x)).exp
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg.h.h.hg
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
⊢ Continuous fun x => (-(Complex.I * ↑x)).exp
Tactic:
. apply Continuous.cexp
  apply Continuous.neg
  apply Continuous.mul
  . apply continuous_const
  . apply Complex.continuous_ofReal
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg.h.h.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun x => 1
Tactic:
apply continuous_const
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case hg.h.h.hg
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
⊢ Continuous fun x => (-(Complex.I * ↑x)).exp
Tactic:
apply Continuous.cexp
Proof state after:
case hg.h.h.hg.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
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
⊢ Continuous fun y => -(Complex.I * ↑y)