internlm/Lean-Github huggingface dataset:
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ DeltaSpike Ψ ε (x / y) = 0
Tactic:
apply DeltaSpikeSupport hε.1 ?_ suppΨ
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ x / y ∉ Icc (2 ^ (-ε)) (2 ^ ε)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x / y
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ x / y ∉ Icc (2 ^ (-ε)) (2 ^ ε)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x / y
Tactic:
simp only [mem_Icc, not_and, not_le]
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x / y
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x / y
Tactic:
swap
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x / y

case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x / y

case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Tactic:
suffices h : 2 ^ ε < x / y by
linarith [(by apply rpow_pos_of_pos (by norm_num) : 0 < (2 : ℝ) ^ ε)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ ε < x / y

case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ ε < x / y

case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Tactic:
all_goals
try intro
have : x / y = ((x / y) ^ (1 / ε)) ^ ε := by
  rw [← rpow_mul]
  simp only [one_div, inv_mul_cancel (ne_of_gt hε.1), rpow_one]
  apply div_nonneg_iff.mpr; left;
  exact ⟨(le_trans (rpow_pos_of_pos (by norm_num) ε).le) hx2.le, ypos.le⟩
rw [this]
refine rpow_lt_rpow (by norm_num) ?_ hε.1
exact Smooth1Properties_above_aux2 hε ⟨ypos, y1⟩ hx2
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ 0 < c
Tactic:
simp only [c, zero_lt_two, mul_pos_iff_of_pos_left]
Proof state after:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ 0 < Real.log 2
Theorem: Smooth1Properties_above
Proof state before:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ 0 < Real.log 2
Tactic:
exact log_pos (by norm_num)
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
h : 2 ^ ε < x / y
⊢ 0 ≤ x / y
Tactic:
linarith [(by apply rpow_pos_of_pos (by norm_num) : 0 < (2 : ℝ) ^ ε)]
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
h : 2 ^ ε < x / y
⊢ 0 < 2 ^ ε
Tactic:
apply rpow_pos_of_pos (by norm_num)
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
h : 2 ^ ε < x / y
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Tactic:
try intro
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y
Tactic:
have : x / y = ((x / y) ^ (1 / ε)) ^ ε := by
  rw [← rpow_mul]
  simp only [one_div, inv_mul_cancel (ne_of_gt hε.1), rpow_one]
  apply div_nonneg_iff.mpr; left;
  exact ⟨(le_trans (rpow_pos_of_pos (by norm_num) ε).le) hx2.le, ypos.le⟩
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 2 ^ ε < x / y
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 2 ^ ε < x / y
Tactic:
rw [this]
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 2 ^ ε < ((x / y) ^ (1 / ε)) ^ ε
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 2 ^ ε < ((x / y) ^ (1 / ε)) ^ ε
Tactic:
refine rpow_lt_rpow (by norm_num) ?_ hε.1
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 2 < (x / y) ^ (1 / ε)
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 2 < (x / y) ^ (1 / ε)
Tactic:
exact Smooth1Properties_above_aux2 hε ⟨ypos, y1⟩ hx2
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Tactic:
intro
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y = ((x / y) ^ (1 / ε)) ^ ε
Tactic:
rw [← rpow_mul]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y = (x / y) ^ (1 / ε * ε)

case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x / y
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y = (x / y) ^ (1 / ε * ε)

case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x / y
Tactic:
simp only [one_div, inv_mul_cancel (ne_of_gt hε.1), rpow_one]
Proof state after:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x / y
Theorem: Smooth1Properties_above
Proof state before:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x / y
Tactic:
apply div_nonneg_iff.mpr
Proof state after:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0
Theorem: Smooth1Properties_above
Proof state before:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0
Tactic:
left
Proof state after:
case hx.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x ∧ 0 ≤ y
Theorem: Smooth1Properties_above
Proof state before:
case hx.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x ∧ 0 ≤ y
Tactic:
exact ⟨(le_trans (rpow_pos_of_pos (by norm_num) ε).le) hx2.le, ypos.le⟩
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
this : x / y = ((x / y) ^ (1 / ε)) ^ ε
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: DeltaSpikeNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ DeltaSpike Ψ ε x
Tactic:
dsimp [DeltaSpike]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Theorem: DeltaSpikeNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Tactic:
have : 0 < x ^ (1 / ε) := by positivity
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this : 0 < x ^ (1 / ε)
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Theorem: DeltaSpikeNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this : 0 < x ^ (1 / ε)
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Tactic:
have : 0 ≤ Ψ (x ^ (1 / ε)) := Ψnonneg _ this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this✝ : 0 < x ^ (1 / ε)
this : 0 ≤ Ψ (x ^ (1 / ε))
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Theorem: DeltaSpikeNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
this✝ : 0 < x ^ (1 / ε)
this : 0 ≤ Ψ (x ^ (1 / ε))
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε
Tactic:
positivity
Proof state after:
no goals
Theorem: DeltaSpikeNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 < x ^ (1 / ε)
Tactic:
positivity
Proof state after:
no goals
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ 0 ≤ MellinConvolution f g x
Tactic:
dsimp [MellinConvolution]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ 0 ≤ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / y
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ 0 ≤ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / y
Tactic:
apply MeasureTheory.setIntegral_nonneg
Proof state after:
case hs
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ MeasurableSet (Ioi 0)

case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ ∀ x_1 ∈ Ioi 0, 0 ≤ f x_1 * g (x / x_1) / x_1
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hs
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ MeasurableSet (Ioi 0)
Tactic:
exact measurableSet_Ioi
Proof state after:
no goals
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
⊢ ∀ x_1 ∈ Ioi 0, 0 ≤ f x_1 * g (x / x_1) / x_1
Tactic:
intro y ypos
Proof state after:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : y ∈ Ioi 0
⊢ 0 ≤ f y * g (x / y) / y
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : y ∈ Ioi 0
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
simp only [mem_Ioi] at ypos
Proof state after:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
⊢ 0 ≤ f y * g (x / y) / y
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
have : 0 ≤ f y := f_nonneg _ ypos
Proof state after:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this : 0 ≤ f y
⊢ 0 ≤ f y * g (x / y) / y
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this : 0 ≤ f y
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
have : 0 < x / y := by positivity
Proof state after:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this✝ : 0 ≤ f y
this : 0 < x / y
⊢ 0 ≤ f y * g (x / y) / y
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this✝ : 0 ≤ f y
this : 0 < x / y
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
have : 0 ≤ g (x / y) := g_nonneg _ this
Proof state after:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this✝¹ : 0 ≤ f y
this✝ : 0 < x / y
this : 0 ≤ g (x / y)
⊢ 0 ≤ f y * g (x / y) / y
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this✝¹ : 0 ≤ f y
this✝ : 0 < x / y
this : 0 ≤ g (x / y)
⊢ 0 ≤ f y * g (x / y) / y
Tactic:
positivity
Proof state after:
no goals
Theorem: MellinConvNonNeg_of_NonNeg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℝ
f_nonneg : ∀ x > 0, 0 ≤ f x
g_nonneg : ∀ x > 0, 0 ≤ g x
x : ℝ
xpos : 0 < x
y : ℝ
ypos : 0 < y
this : 0 ≤ f y
⊢ 0 < x / y
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Nonneg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Smooth1 Ψ ε x
Tactic:
dsimp [Smooth1]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ MellinConvolution (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike Ψ ε) x
Theorem: Smooth1Nonneg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ MellinConvolution (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike Ψ ε) x
Tactic:
apply MellinConvNonNeg_of_NonNeg ?_ ?_ xpos
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ if 0 < x ∧ x ≤ 1 then 1 else 0

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ DeltaSpike Ψ ε x
Theorem: Smooth1Nonneg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ if 0 < x ∧ x ≤ 1 then 1 else 0
Tactic:
intro y hy
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
hy : y > 0
⊢ 0 ≤ if 0 < y ∧ y ≤ 1 then 1 else 0
Theorem: Smooth1Nonneg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
hy : y > 0
⊢ 0 ≤ if 0 < y ∧ y ≤ 1 then 1 else 0
Tactic:
by_cases h : y ≤ 1 <;> simp [h, hy]
Proof state after:
no goals
Theorem: Smooth1Nonneg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ ∀ x > 0, 0 ≤ DeltaSpike Ψ ε x
Tactic:
intro y ypos
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
ypos : y > 0
⊢ 0 ≤ DeltaSpike Ψ ε y
Theorem: Smooth1Nonneg
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
ε x : ℝ
xpos : 0 < x
εpos : 0 < ε
y : ℝ
ypos : y > 0
⊢ 0 ≤ DeltaSpike Ψ ε y
Tactic:
exact DeltaSpikeNonNeg_of_NonNeg Ψnonneg ypos εpos
Proof state after:
no goals