internlm/Lean-Github huggingface dataset:
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Tactic:
. calc ‖k (-y) - 0‖
    _ = ‖k (-y) - k (-1)‖ := by
      congr
      apply (k_of_one_le_abs _).symm
      simp
    _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by
      apply Hilbert_kernel_regularity_main_part
      constructor
      all_goals linarith
    _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
      rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
    _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr <;> norm_num
Proof state after:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Tactic:
. rw [abs_neg, abs_of_nonneg] <;> linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
calc ‖k (-y) - 0‖
  _ = ‖k (-y) - k (-1)‖ := by
    congr
    apply (k_of_one_le_abs _).symm
    simp
  _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by
    apply Hilbert_kernel_regularity_main_part
    constructor
    all_goals linarith
  _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
    rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
  _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr <;> norm_num
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - 0‖ = ‖k (-y) - k (-1)‖
Tactic:
congr
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 = k (-1)
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 = k (-1)
Tactic:
apply (k_of_one_le_abs _).symm
Proof state after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-1)|
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-1)|
Tactic:
simp
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ ‖k (-y) - k (-1)‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|)
Tactic:
apply Hilbert_kernel_regularity_main_part
Proof state after:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Theorem: Hilbert_kernel_regularity
Proof state before:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Tactic:
constructor
Proof state after:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Theorem: Hilbert_kernel_regularity
Proof state before:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ y

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 0 < y

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ y ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Tactic:
all_goals linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|)
Proof state after:
case h.hab
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - 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'|
Theorem: Hilbert_kernel_regularity
Proof state before:
case h.hab
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - 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'|
Tactic:
rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr <;> norm_num
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inl.inr
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' > 1
⊢ 1 ≤ |(-y')|
Tactic:
rw [abs_neg, abs_of_nonneg] <;> linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - 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 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [@k_of_one_le_abs (-y)]
Proof state after:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Tactic:
. calc ‖0 - k (-y')‖
    _ = ‖k (-1) - k (-y')‖ := by
      congr
      apply (k_of_one_le_abs _).symm
      simp
    _ = ‖k (-y') - k (-1)‖ := by
      rw [norm_sub_rev]
    _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by
      apply Hilbert_kernel_regularity_main_part
      constructor
      all_goals linarith
    _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by
      congr
      . rw [abs_of_nonneg]
        exact yy'nonneg.2
      . rw [abs_of_nonpos]
        simp
        linarith
      . rw [abs_of_nonneg]
        exact yy'nonneg.2
    _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by
      gcongr
      . apply div_nonneg <;> linarith
      . linarith
    _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by
      ring
    _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr
      apply div_nonneg <;> linarith
      rw [abs_of_nonneg yy'nonneg.1]
      rw [abs_of_nonneg] <;> linarith
      rw [abs_of_nonneg yy'nonneg.1]
    _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
      gcongr
      norm_num
Proof state after:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-y)|
Tactic:
. rw [abs_neg, abs_of_nonneg] <;> linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inr.inl
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
calc ‖0 - k (-y')‖
  _ = ‖k (-1) - k (-y')‖ := by
    congr
    apply (k_of_one_le_abs _).symm
    simp
  _ = ‖k (-y') - k (-1)‖ := by
    rw [norm_sub_rev]
  _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by
    apply Hilbert_kernel_regularity_main_part
    constructor
    all_goals linarith
  _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by
    congr
    . rw [abs_of_nonneg]
      exact yy'nonneg.2
    . rw [abs_of_nonpos]
      simp
      linarith
    . rw [abs_of_nonneg]
      exact yy'nonneg.2
  _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by
    gcongr
    . apply div_nonneg <;> linarith
    . linarith
  _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by
    ring
  _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr
    apply div_nonneg <;> linarith
    rw [abs_of_nonneg yy'nonneg.1]
    rw [abs_of_nonneg] <;> linarith
    rw [abs_of_nonneg yy'nonneg.1]
  _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
    gcongr
    norm_num
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖0 - k (-y')‖ = ‖k (-1) - k (-y')‖
Tactic:
congr
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 = k (-1)
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 = k (-1)
Tactic:
apply (k_of_one_le_abs _).symm
Proof state after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-1)|
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ |(-1)|
Tactic:
simp
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-1) - k (-y')‖ = ‖k (-y') - k (-1)‖
Tactic:
rw [norm_sub_rev]
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ ‖k (-y') - k (-1)‖ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|)
Tactic:
apply Hilbert_kernel_regularity_main_part
Proof state after:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y' ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Theorem: Hilbert_kernel_regularity
Proof state before:
case yy'nonneg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y' ∧ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Tactic:
constructor
Proof state after:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Theorem: Hilbert_kernel_regularity
Proof state before:
case yy'nonneg.left
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'

case yy'nonneg.right
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ 1

case ypos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 < y'

case y2ley'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' / 2 ≤ 1

case hy
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' ≤ 1

case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Tactic:
all_goals linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case hy'
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 1 ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) = 2 ^ 6 * (1 / y') * ((1 - y') / y')
Tactic:
congr
Proof state after:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
. rw [abs_of_nonneg]
  exact yy'nonneg.2
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
. rw [abs_of_nonpos]
  simp
  linarith
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
. rw [abs_of_nonneg]
  exact yy'nonneg.2
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
rw [abs_of_nonneg]
Proof state after:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'
Tactic:
exact yy'nonneg.2
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y' - 1| = 1 - y'
Tactic:
rw [abs_of_nonpos]
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ -(y' - 1) = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ -(y' - 1) = 1 - y'

case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0
Tactic:
simp
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ y' - 1 ≤ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ |y'| = y'
Tactic:
rw [abs_of_nonneg]
Proof state after:
case e_a.e_a
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 0 ≤ y'