internlm/Lean-Github huggingface dataset:
Theorem: Hilbert_kernel_regularity
Proof state before:
x y y' : ℝ
x_eq_zero : x = 0
⊢ 2 * |y - y'| ≤ |0 - y| → ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Tactic:
intro h
Proof state after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |0 - y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |0 - y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Tactic:
simp at h
Proof state after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (0 - y) - k (0 - y')‖ ≤ 2 ^ 8 * (1 / |0 - y|) * (|y - y'| / |0 - y|)
Tactic:
simp only [zero_sub, abs_neg]
Proof state after:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
wlog yy'nonneg : 0 ≤ y ∧ 0 ≤ y' generalizing y y'
Proof state after:
case inr
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. by_cases yge0 : 0 ≤ y
  . push_neg at yy'nonneg
    exfalso
    rw [abs_of_nonneg yge0, abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]
  . push_neg at yge0
    by_cases y'ge0 : 0 ≤ y'
    . exfalso
      rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
    . push_neg at y'ge0
      set! y_ := -y with y_def
      set! y'_ := -y' with y'_def
      have h_ : 2 * |y_ - y'_| ≤ |y_| := by
        rw [y_def, y'_def, ← abs_neg]
        simpa [neg_add_eq_sub]
      have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
      have := this h_ y_y'_nonneg
      rw [y_def, y'_def] at this
      simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
      rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
      simpa
Proof state after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
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'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
by_cases ypos : y ≤ 0
Proof state after:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case pos
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. have y_eq_zero : y = 0 := by
    exact le_antisymm ypos yy'nonneg.1
  have y'_eq_zero : y' = 0 := by
    rw [y_eq_zero] at h
    simp at h
    rw [abs_of_nonneg yy'nonneg.2] at h
    linarith
  rw [y_eq_zero, y'_eq_zero]
  simp
Proof state after:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : ¬y ≤ 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at ypos
Proof state after:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have y2ley' : y / 2 ≤ y' := by
  rw [div_le_iff two_pos]
  calc y
    _ = 2 * (y - y') - y + 2 * y' := by ring
    _ ≤ 2 * |y - y'| - y + 2 * y' := by
      gcongr
      apply le_abs_self
    _ ≤ y - y + 2 * y' := by
      gcongr
      rw [abs_eq_self.mpr yy'nonneg.1] at h
      exact h
    _ = y' * 2 := by ring
Proof state after:
case neg
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'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg
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'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rcases le_or_gt y 1, le_or_gt y' 1 with ⟨hy | hy, hy' | hy'⟩
Proof state after:
case neg.inl.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|)

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) - 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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inl.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|)

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) - 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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy')
  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
⊢ ‖k (-y) - 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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |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
⊢ ‖k (-y) - 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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. rw [@k_of_one_le_abs (-y')]
  . 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
  . rw [abs_neg, abs_of_nonneg] <;> linarith
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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. rw [@k_of_one_le_abs (-y)]
  . 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
  . rw [abs_neg, abs_of_nonneg] <;> linarith
Proof state after:
case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg.inr.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) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. calc ‖k (-y) - k (-y')‖
    _ = 0 := by
      simp
      rw [k_of_one_le_abs, k_of_one_le_abs] <;> (rw [abs_neg, abs_of_nonneg] <;> linarith)
    _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by
      apply mul_nonneg
      apply mul_nonneg
      . norm_num
      . simp
      . apply div_nonneg <;> simp
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
⊢ 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
intro h
Proof state after:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
h : 2 * |y - y'| ≤ |x - y|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
this :
  ∀ {x y y' : ℝ},
    x = 0 → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = 0
h : 2 * |y - y'| ≤ |x - y|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
set x_ := (0 : ℝ) with x_def
Proof state after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
set y_ := y - x with y_def
Proof state after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
set y'_ := y' - x with y'_def
Proof state after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
have h_ : 2 * |y_ - y'_| ≤ |x_ - y_| := by
  rw [x_def, y_def, y'_def]
  simpa
Proof state after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
have := this x_def h_
Proof state after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (x_ - y_) - k (x_ - y'_)‖ ≤ 2 ^ 8 * (1 / |x_ - y_|) * (|y_ - y'_| / |x_ - y_|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (x_ - y_) - k (x_ - y'_)‖ ≤ 2 ^ 8 * (1 / |x_ - y_|) * (|y_ - y'_| / |x_ - y_|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
rw [x_def, y_def, y'_def] at this
Proof state after:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (0 - (y - x)) - k (0 - (y' - x))‖ ≤ 2 ^ 8 * (1 / |0 - (y - x)|) * (|y - x - (y' - x)| / |0 - (y - x)|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this✝ :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
h_ : 2 * |y_ - y'_| ≤ |x_ - y_|
this : ‖k (0 - (y - x)) - k (0 - (y' - x))‖ ≤ 2 ^ 8 * (1 / |0 - (y - x)|) * (|y - x - (y' - x)| / |0 - (y - x)|)
⊢ ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
Tactic:
simpa
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ 2 * |y_ - y'_| ≤ |x_ - y_|
Tactic:
rw [x_def, y_def, y'_def]
Proof state after:
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ 2 * |y - x - (y' - x)| ≤ |0 - (y - x)|
Theorem: Hilbert_kernel_regularity
Proof state before:
x y y' : ℝ
h : 2 * |y - y'| ≤ |x - y|
x_ : ℝ := 0
this :
  ∀ {x y y' : ℝ},
    x = x_ → 2 * |y - y'| ≤ |x - y| → ‖k (x - y) - k (x - y')‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)
x_eq_zero : ¬x = x_
x_def : x_ = 0
y_ : ℝ := y - x
y_def : y_ = y - x
y'_ : ℝ := y' - x
y'_def : y'_ = y' - x
⊢ 2 * |y - x - (y' - x)| ≤ |0 - (y - x)|
Tactic:
simpa
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case inr
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
by_cases yge0 : 0 ≤ y
Proof state after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : 0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : 0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)

case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. push_neg at yy'nonneg
  exfalso
  rw [abs_of_nonneg yge0, abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]
Proof state after:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Theorem: Hilbert_kernel_regularity
Proof state before:
case neg
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : ¬0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. push_neg at yge0
  by_cases y'ge0 : 0 ≤ y'
  . exfalso
    rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
  . push_neg at y'ge0
    set! y_ := -y with y_def
    set! y'_ := -y' with y'_def
    have h_ : 2 * |y_ - y'_| ≤ |y_| := by
      rw [y_def, y'_def, ← abs_neg]
      simpa [neg_add_eq_sub]
    have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
    have := this h_ y_y'_nonneg
    rw [y_def, y'_def] at this
    simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
    rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
    simpa
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yy'nonneg : ¬(0 ≤ y ∧ 0 ≤ y')
yge0 : 0 ≤ y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at yy'nonneg
Proof state after:
case pos
x y y' : ℝ
x_eq_zero : x = 0
h : 2 * |y - y'| ≤ |y|
this : ∀ {y y' : ℝ}, 2 * |y - y'| ≤ |y| → 0 ≤ y ∧ 0 ≤ y' → ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)