internlm/Lean-Github huggingface dataset:
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 ≤ y'
Tactic:
exact yy'nonneg.2
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') * ((1 - y') / y') ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2))
Tactic:
gcongr
Proof state after:
case c0
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 - y') / y'

case h₂.ha
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 - y'
Theorem: Hilbert_kernel_regularity
Proof state before:
case c0
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 - y') / y'

case h₂.ha
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 - y'
Tactic:
. apply div_nonneg <;> linarith
Proof state after:
case h₂.ha
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 - y'
Theorem: Hilbert_kernel_regularity
Proof state before:
case h₂.ha
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 - y'
Tactic:
. linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case c0
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 - y') / y'
Tactic:
apply div_nonneg <;> linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case h₂.ha
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 - y'
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 / 2)) * ((1 - y') / (y / 2)) = 2 ^ 6 * 2 * 2 * (1 / y) * ((1 - y') / 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
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * 2 * 2 * (1 / y) * ((1 - y') / y) ≤ 2 ^ 6 * 2 * 2 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr
Proof state after:
case c0
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 - y') / y

case h₁.h.h
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 h₂.hac
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' ≤ |y - y'|

case h₂.hbd
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 c0
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 - y') / y

case h₁.h.h
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 h₂.hac
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' ≤ |y - y'|

case h₂.hbd
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:
apply div_nonneg <;> linarith
Proof state after:
case h₁.h.h
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 h₂.hac
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' ≤ |y - y'|

case h₂.hbd
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 h₁.h.h
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 h₂.hac
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' ≤ |y - y'|

case h₂.hbd
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 yy'nonneg.1]
Proof state after:
case h₂.hac
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' ≤ |y - y'|

case h₂.hbd
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 h₂.hac
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' ≤ |y - y'|

case h₂.hbd
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] <;> linarith
Proof state after:
case h₂.hbd
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 h₂.hbd
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 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 : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' ≤ 1
⊢ 2 ^ 6 * 2 * 2 * (1 / |y|) * (|y - y'| / |y|) ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
gcongr
Proof state after:
case h.h
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 * 2 * 2 ≤ 2 ^ 8
Theorem: Hilbert_kernel_regularity
Proof state before:
case h.h
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 * 2 * 2 ≤ 2 ^ 8
Tactic:
norm_num
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
⊢ 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.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:
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')‖ = 0
Tactic:
simp
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
⊢ k (-y) = k (-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'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y > 1
hy' : y' > 1
⊢ k (-y) = k (-y')
Tactic:
rw [k_of_one_le_abs, k_of_one_le_abs] <;> (rw [abs_neg, 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
⊢ 1 ≤ |(-y)|
Tactic:
rw [abs_neg, 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
⊢ 0 ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
apply mul_nonneg
Proof state after:
case ha
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 ≤ 2 ^ 8 * (1 / |y|)

case hb
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 - y'| / |y|
Theorem: Hilbert_kernel_regularity
Proof state before:
case ha
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 ≤ 2 ^ 8 * (1 / |y|)

case hb
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 - y'| / |y|
Tactic:
apply mul_nonneg
Proof state after:
case ha.ha
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 ≤ 2 ^ 8

case ha.hb
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 / |y|

case hb
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 - y'| / |y|
Theorem: Hilbert_kernel_regularity
Proof state before:
case ha.ha
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 ≤ 2 ^ 8

case ha.hb
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 / |y|

case hb
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 - y'| / |y|
Tactic:
. norm_num
Proof state after:
case ha.hb
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 / |y|

case hb
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 - y'| / |y|
Theorem: Hilbert_kernel_regularity
Proof state before:
case ha.hb
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 / |y|

case hb
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 - y'| / |y|
Tactic:
. simp
Proof state after:
case hb
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 - y'| / |y|
Theorem: Hilbert_kernel_regularity
Proof state before:
case hb
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 - y'| / |y|
Tactic:
. apply div_nonneg <;> simp
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case ha.ha
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 ≤ 2 ^ 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case ha.hb
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 / |y|
Tactic:
simp
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity
Proof state before:
case hb
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 - y'| / |y|
Tactic:
apply div_nonneg <;> simp
Proof state after:
no goals
Theorem: C1_2_pos
Proof state before:
a q : ℝ
hq : 1 < q
⊢ 0 < C1_2 a q
Tactic:
rw [C1_2]
Proof state after:
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3) / (q - 1) ^ 5
Theorem: C1_2_pos
Proof state before:
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3) / (q - 1) ^ 5
Tactic:
apply div_pos
Proof state after:
case ha
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3)

case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Theorem: C1_2_pos
Proof state before:
case ha
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3)

case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Tactic:
. apply Real.rpow_pos_of_pos
  norm_num
Proof state after:
case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Theorem: C1_2_pos
Proof state before:
case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Tactic:
. apply pow_pos
  linarith [hq]
Proof state after:
no goals
Theorem: C1_2_pos
Proof state before:
case ha
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3)
Tactic:
apply Real.rpow_pos_of_pos
Proof state after:
case ha.hx
a q : ℝ
hq : 1 < q
⊢ 0 < 2
Theorem: C1_2_pos
Proof state before:
case ha.hx
a q : ℝ
hq : 1 < q
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: C1_2_pos
Proof state before:
case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Tactic:
apply pow_pos
Proof state after:
case hb.H
a q : ℝ
hq : 1 < q
⊢ 0 < q - 1
Theorem: C1_2_pos
Proof state before:
case hb.H
a q : ℝ
hq : 1 < q
⊢ 0 < q - 1
Tactic:
linarith [hq]
Proof state after:
no goals
Theorem: Int.floor_le_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x y : X
hD : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
c : ℝ
z : ℤ
⊢ ⌊c⌋ ≤ z ↔ c < ↑z + 1
Tactic:
rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right]
Proof state after:
no goals
Theorem: Int.le_ceil_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x y : X
hD : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
c : ℝ
z : ℤ
⊢ z ≤ ⌈c⌉ ↔ ↑z - 1 < c
Tactic:
rw_mod_cast [← Int.add_one_le_ceil_iff, sub_add_cancel]
Proof state after:
no goals
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ i ∈ nonzeroS D x ↔ D ^ i * x ∈ Ioo (4 * D)⁻¹ 2⁻¹
Tactic:
rw [Set.mem_Ioo, nonzeroS, Finset.mem_Icc]
Proof state after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ ⌊-D.logb (4 * x)⌋ ≤ i ∧ i ≤ ⌈-(1 + D.logb (2 * x))⌉ ↔ (4 * D)⁻¹ < D ^ i * x ∧ D ^ i * x < 2⁻¹
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ ⌊-D.logb (4 * x)⌋ ≤ i ∧ i ≤ ⌈-(1 + D.logb (2 * x))⌉ ↔ (4 * D)⁻¹ < D ^ i * x ∧ D ^ i * x < 2⁻¹
Tactic:
simp only [Int.floor_le_iff, neg_add_rev, Int.le_ceil_iff, lt_add_neg_iff_add_lt, sub_add_cancel,
  mul_inv_rev]
Proof state after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ -D.logb (4 * x) < ↑i + 1 ∧ ↑i < -D.logb (2 * x) ↔ D⁻¹ * 4⁻¹ < D ^ i * x ∧ D ^ i * x < 2⁻¹
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ -D.logb (4 * x) < ↑i + 1 ∧ ↑i < -D.logb (2 * x) ↔ D⁻¹ * 4⁻¹ < D ^ i * x ∧ D ^ i * x < 2⁻¹
Tactic:
rw [← lt_div_iff hx, mul_comm D⁻¹, ← div_lt_div_iff hx (by positivity), ← Real.logb_inv,
  ← Real.logb_inv, div_inv_eq_mul, ← zpow_add_one₀ (by positivity)]
Proof state after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ D.logb (4 * x)⁻¹ < ↑i + 1 ∧ ↑i < D.logb (2 * x)⁻¹ ↔ 4⁻¹ / x < D ^ (i + 1) ∧ D ^ i < 2⁻¹ / x
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ D.logb (4 * x)⁻¹ < ↑i + 1 ∧ ↑i < D.logb (2 * x)⁻¹ ↔ 4⁻¹ / x < D ^ (i + 1) ∧ D ^ i < 2⁻¹ / x
Tactic:
simp_rw [← Real.rpow_intCast]
Proof state after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ D.logb (4 * x)⁻¹ < ↑i + 1 ∧ ↑i < D.logb (2 * x)⁻¹ ↔ 4⁻¹ / x < D ^ ↑(i + 1) ∧ D ^ ↑i < 2⁻¹ / x
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ D.logb (4 * x)⁻¹ < ↑i + 1 ∧ ↑i < D.logb (2 * x)⁻¹ ↔ 4⁻¹ / x < D ^ ↑(i + 1) ∧ D ^ ↑i < 2⁻¹ / x
Tactic:
rw [Real.lt_logb_iff_rpow_lt hD (by positivity), Real.logb_lt_iff_lt_rpow hD (by positivity)]
Proof state after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ (4 * x)⁻¹ < D ^ (↑i + 1) ∧ D ^ ↑i < (2 * x)⁻¹ ↔ 4⁻¹ / x < D ^ ↑(i + 1) ∧ D ^ ↑i < 2⁻¹ / x
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ (4 * x)⁻¹ < D ^ (↑i + 1) ∧ D ^ ↑i < (2 * x)⁻¹ ↔ 4⁻¹ / x < D ^ ↑(i + 1) ∧ D ^ ↑i < 2⁻¹ / x
Tactic:
simp [div_eq_mul_inv, mul_comm]
Proof state after:
no goals
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ 0 < D⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: mem_nonzeroS_iff
Proof state before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x✝ y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ D ≠ 0
Tactic:
positivity
Proof state after:
no goals