internlm/Lean-Github huggingface dataset:
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|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
exfalso
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
⊢ False
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|)
yge0 : 0 ≤ y
yy'nonneg : 0 ≤ y → y' < 0
⊢ False
Tactic:
rw [abs_of_nonneg yge0, abs_of_nonneg] at h <;> linarith [yy'nonneg yge0]
Proof state after:
no goals
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
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 : y < 0
⊢ ‖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 : y < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
by_cases y'ge0 : 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 : y < 0
y'ge0 : 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 : y < 0
y'ge0 : ¬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 : y < 0
y'ge0 : 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 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. exfalso
  rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
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 : y < 0
y'ge0 : ¬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 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
. 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 : y < 0
y'ge0 : 0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
exfalso
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 : y < 0
y'ge0 : 0 ≤ y'
⊢ False
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 : y < 0
y'ge0 : 0 ≤ y'
⊢ False
Tactic:
rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith
Proof state after:
no goals
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 : y < 0
y'ge0 : ¬0 ≤ y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
push_neg at y'ge0
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 : y < 0
y'ge0 : y' < 0
⊢ ‖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 : y < 0
y'ge0 : y' < 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
set! y_ := -y with y_def
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
set! y'_ := -y' with y'_def
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have h_ : 2 * |y_ - y'_| ≤ |y_| := by
  rw [y_def, y'_def, ← abs_neg]
  simpa [neg_add_eq_sub]
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
have := this h_ y_y'_nonneg
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y_) - k (-y'_)‖ ≤ 2 ^ 8 * (1 / |y_|) * (|y_ - y'_| / |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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y_) - k (-y'_)‖ ≤ 2 ^ 8 * (1 / |y_|) * (|y_ - y'_| / |y_|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [y_def, y'_def] at this
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (- -y) - k (- -y')‖ ≤ 2 ^ 8 * (1 / |(-y)|) * (|-y - -y'| / |(-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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (- -y) - k (- -y')‖ ≤ 2 ^ 8 * (1 / |(-y)|) * (|-y - -y'| / |(-y)|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k y - k y'‖ ≤ 2 ^ 8 * (1 / |y|) * (|y' - y| / |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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k y - k y'‖ ≤ 2 ^ 8 * (1 / |y|) * (|y' - y| / |y|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|(-(y' - y))| / |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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_
this : ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|(-(y' - y))| / |y|)
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
simpa
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ 2 * |y_ - y'_| ≤ |y_|
Tactic:
rw [y_def, y'_def, ← abs_neg]
Proof state after:
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ 2 * |(-(-y - -y'))| ≤ |(-y)|
Theorem: Hilbert_kernel_regularity
Proof state before:
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
⊢ 2 * |(-(-y - -y'))| ≤ |(-y)|
Tactic:
simpa [neg_add_eq_sub]
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
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 : y < 0
y'ge0 : y' < 0
y_ : ℝ := -y
y_def : y_ = -y
y'_ : ℝ := -y'
y'_def : y'_ = -y'
h_ : 2 * |y_ - y'_| ≤ |y_|
⊢ 0 ≤ y_ ∧ 0 ≤ y'_
Tactic:
constructor <;> linarith
Proof state after:
no goals
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|)
Tactic:
have y_eq_zero : y = 0 := by
  exact le_antisymm ypos yy'nonneg.1
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
y_eq_zero : 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
y_eq_zero : y = 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
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
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
y_eq_zero : y = 0
y'_eq_zero : 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
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [y_eq_zero, y'_eq_zero]
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
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-0) - k (-0)‖ ≤ 2 ^ 8 * (1 / |0|) * (|0 - 0| / |0|)
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
y_eq_zero : y = 0
y'_eq_zero : y' = 0
⊢ ‖k (-0) - k (-0)‖ ≤ 2 ^ 8 * (1 / |0|) * (|0 - 0| / |0|)
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 : y ≤ 0
⊢ y = 0
Tactic:
exact le_antisymm ypos yy'nonneg.1
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 : y ≤ 0
y_eq_zero : y = 0
⊢ y' = 0
Tactic:
rw [y_eq_zero] at h
Proof state after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |0 - y'| ≤ |0|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ y' = 0
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |0 - y'| ≤ |0|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
⊢ y' = 0
Tactic:
simp at h
Proof state after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * |y'| ≤ 0
⊢ y' = 0
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * |y'| ≤ 0
⊢ y' = 0
Tactic:
rw [abs_of_nonneg yy'nonneg.2] at h
Proof state after:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * y' ≤ 0
⊢ y' = 0
Theorem: Hilbert_kernel_regularity
Proof state before:
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : y ≤ 0
y_eq_zero : y = 0
h : 2 * y' ≤ 0
⊢ y' = 0
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
⊢ y / 2 ≤ y'
Tactic:
rw [div_le_iff two_pos]
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
⊢ y ≤ y' * 2
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
⊢ y ≤ y' * 2
Tactic:
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:
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
⊢ y = 2 * (y - y') - y + 2 * y'
Tactic:
ring
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
⊢ 2 * (y - y') - y + 2 * y' ≤ 2 * |y - y'| - y + 2 * y'
Tactic:
gcongr
Proof state after:
case bc.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y - y' ≤ |y - y'|
Theorem: Hilbert_kernel_regularity
Proof state before:
case bc.h.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ y - y' ≤ |y - y'|
Tactic:
apply le_abs_self
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
⊢ 2 * |y - y'| - y + 2 * y' ≤ y - y + 2 * y'
Tactic:
gcongr
Proof state after:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y
Theorem: Hilbert_kernel_regularity
Proof state before:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ |y|
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y
Tactic:
rw [abs_eq_self.mpr yy'nonneg.1] at h
Proof state after:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ y
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y
Theorem: Hilbert_kernel_regularity
Proof state before:
case bc.h
x : ℝ
x_eq_zero : x = 0
y y' : ℝ
h : 2 * |y - y'| ≤ y
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
⊢ 2 * |y - y'| ≤ y
Tactic:
exact h
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
⊢ y - y + 2 * y' = y' * 2
Tactic:
ring
Proof state after:
no goals
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|)
Tactic:
apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' 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
⊢ 2 ^ 6 * (1 / |y|) * (|y - y'| / |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
⊢ 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
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [@k_of_one_le_abs (-y')]
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) - 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')|