internlm/Lean-Github huggingface dataset:
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Tactic:
have pos: 0 < (1 - 2 ^ (-ε)) / ε := by
  refine div_pos ?_ hε.1
  rw [sub_pos, ← pow_zero 2]
  convert rpow_lt_rpow_of_exponent_lt (x := 2) (by norm_num) (neg_lt_zero.mpr hε.1); norm_num
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Tactic:
have := (mul_lt_mul_right pos).mpr this
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this✝ : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
this : 2 ^ ε * ((1 - 2 ^ (-ε)) / ε) < 2 * ((1 - 2 ^ (-ε)) / ε)
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this✝ : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
this : 2 ^ ε * ((1 - 2 ^ (-ε)) / ε) < 2 * ((1 - 2 ^ (-ε)) / ε)
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Tactic:
ring_nf at this ⊢
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this✝ : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
this : -(2 ^ ε * 2 ^ (-ε) * ε⁻¹) + 2 ^ ε * ε⁻¹ < -(2 ^ (-ε) * ε⁻¹ * 2) + ε⁻¹ * 2
⊢ -(2 ^ (-ε) * ε⁻¹ * 2) + ε⁻¹ * 2 > -(2 ^ ε * 2 ^ (-ε) * ε⁻¹) + 2 ^ ε * ε⁻¹
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this✝ : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
this : -(2 ^ ε * 2 ^ (-ε) * ε⁻¹) + 2 ^ ε * ε⁻¹ < -(2 ^ (-ε) * ε⁻¹ * 2) + ε⁻¹ * 2
⊢ -(2 ^ (-ε) * ε⁻¹ * 2) + ε⁻¹ * 2 > -(2 ^ ε * 2 ^ (-ε) * ε⁻¹) + 2 ^ ε * ε⁻¹
Tactic:
exact this
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε < 2
Tactic:
nth_rewrite 1 [← pow_one 2]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ 1) ^ ε < 2
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ 1) ^ ε < 2
Tactic:
convert rpow_lt_rpow_of_exponent_lt (x := 2) (by norm_num) hε.2 <;> norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 0 < (1 - 2 ^ (-ε)) / ε
Tactic:
refine div_pos ?_ hε.1
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 0 < 1 - 2 ^ (-ε)
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 0 < 1 - 2 ^ (-ε)
Tactic:
rw [sub_pos, ← pow_zero 2]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 ^ (-ε) < 2 ^ 0
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 ^ (-ε) < 2 ^ 0
Tactic:
convert rpow_lt_rpow_of_exponent_lt (x := 2) (by norm_num) (neg_lt_zero.mpr hε.1)
Proof state after:
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 ^ 0 = 2 ^ 0
Theorem: Smooth1Properties_above_aux
Proof state before:
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 ^ 0 = 2 ^ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε * (1 - 2 ^ (-ε)) / ε = (2 ^ ε - 1) / ε
Tactic:
have : (2 : ℝ) ^ ε * (2 : ℝ) ^ (-ε) = (2 : ℝ) ^ (ε - ε) := by
  rw [← rpow_add (by norm_num), add_neg_self, sub_self]
Proof state after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε * 2 ^ (-ε) = 2 ^ (ε - ε)
⊢ 2 ^ ε * (1 - 2 ^ (-ε)) / ε = (2 ^ ε - 1) / ε
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε * 2 ^ (-ε) = 2 ^ (ε - ε)
⊢ 2 ^ ε * (1 - 2 ^ (-ε)) / ε = (2 ^ ε - 1) / ε
Tactic:
conv => lhs; lhs; ring_nf; rhs; simp [this]
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε * 2 ^ (-ε) = 2 ^ (ε - ε)
Tactic:
rw [← rpow_add (by norm_num), add_neg_self, sub_self]
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hε : ε ∈ Ioo 0 1
hy : y ∈ Ioc 0 1
hx2 : 2 ^ ε < x
⊢ 2 < (x / y) ^ (1 / ε)
Tactic:
obtain ⟨εpos, ε1⟩ := hε
Proof state after:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hy : y ∈ Ioc 0 1
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
⊢ 2 < (x / y) ^ (1 / ε)
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hy : y ∈ Ioc 0 1
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
⊢ 2 < (x / y) ^ (1 / ε)
Tactic:
obtain ⟨ypos, y1⟩ := hy
Proof state after:
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 < (x / y) ^ (1 / ε)
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 < (x / y) ^ (1 / ε)
Tactic:
calc
  _ > (2 ^ ε / y) ^ (1 / ε) := ?_
  _ = 2 / y ^ (1 / ε) := ?_
  _ ≥ 2 / y := ?_
  _ ≥ 2 := ?_
Proof state after:
case intro.intro.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (x / y) ^ (1 / ε) > (2 ^ ε / y) ^ (1 / ε)

case intro.intro.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (2 ^ ε / y) ^ (1 / ε) = 2 / y ^ (1 / ε)

case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 / y ^ (1 / ε) ≥ 2 / y

case intro.intro.calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 / y ≥ 2
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (x / y) ^ (1 / ε) > (2 ^ ε / y) ^ (1 / ε)
Tactic:
rw [gt_iff_lt, div_rpow, div_rpow, lt_div_iff, mul_comm_div, div_self, mul_one]
<;> try positivity
Proof state after:
case intro.intro.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (2 ^ ε) ^ (1 / ε) < x ^ (1 / ε)

case intro.intro.calc_1.hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_1.hy
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ y
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (2 ^ ε) ^ (1 / ε) < x ^ (1 / ε)
Tactic:
exact rpow_lt_rpow (by positivity) hx2 (by positivity)
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ 2 ^ ε
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 < 1 / ε
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_1.hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 ≤ x
Tactic:
exact LT.lt.le <| lt_trans (by positivity) hx2
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 0 < 2 ^ ε
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (2 ^ ε / y) ^ (1 / ε) = 2 / y ^ (1 / ε)
Tactic:
rw [div_rpow, ← rpow_mul, mul_div_cancel₀ 1 <| ne_of_gt εpos, rpow_one] <;> positivity
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 / y ^ (1 / ε) ≥ 2 / y
Tactic:
have : y ^ (1 / ε) ≤ y := by
  nth_rewrite 2 [← rpow_one y]
  exact rpow_le_rpow_of_exponent_ge ypos y1 (by linarith [one_lt_one_div εpos ε1])
Proof state after:
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
this : y ^ (1 / ε) ≤ y
⊢ 2 / y ^ (1 / ε) ≥ 2 / y
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
this : y ^ (1 / ε) ≤ y
⊢ 2 / y ^ (1 / ε) ≥ 2 / y
Tactic:
have pos : 0 < y ^ (1 / ε) := rpow_pos_of_pos ypos _
Proof state after:
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
this : y ^ (1 / ε) ≤ y
pos : 0 < y ^ (1 / ε)
⊢ 2 / y ^ (1 / ε) ≥ 2 / y
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
this : y ^ (1 / ε) ≤ y
pos : 0 < y ^ (1 / ε)
⊢ 2 / y ^ (1 / ε) ≥ 2 / y
Tactic:
rw [ge_iff_le, div_le_iff, div_mul_eq_mul_div, le_div_iff', mul_comm] <;> try linarith
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ y ^ (1 / ε) ≤ y
Tactic:
nth_rewrite 2 [← rpow_one y]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ y ^ (1 / ε) ≤ y ^ 1
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ y ^ (1 / ε) ≤ y ^ 1
Tactic:
exact rpow_le_rpow_of_exponent_ge ypos y1 (by linarith [one_lt_one_div εpos ε1])
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 1 ≤ 1 / ε
Tactic:
linarith [one_lt_one_div εpos ε1]
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
this : y ^ (1 / ε) ≤ y
pos : 0 < y ^ (1 / ε)
⊢ 0 < y
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 / y ≥ 2
Tactic:
rw [ge_iff_le, le_div_iff <| ypos]
Proof state after:
case intro.intro.calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 * y ≤ 2
Theorem: Smooth1Properties_above_aux2
Proof state before:
case intro.intro.calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ 2 * y ≤ 2
Tactic:
exact (mul_le_iff_le_one_right zero_lt_two).mpr y1
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, 0 < c ∧ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
Tactic:
set c := 2 * Real.log 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
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
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
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
Tactic:
use c
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ 0 < c ∧ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
Theorem: Smooth1Properties_above
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ 0 < c ∧ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
Tactic:
constructor
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 < c

case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
⊢ ∀ (x : ℝ), 1 + c * ε ≤ x → Smooth1 Ψ ε x = 0
Tactic:
intro x hx
Proof state after:
case h.right
𝕂 : 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
⊢ Smooth1 Ψ ε x = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right
𝕂 : 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
⊢ Smooth1 Ψ ε x = 0
Tactic:
have hx2 := Smooth1Properties_above_aux hx hε
Proof state after:
case h.right
𝕂 : 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
⊢ Smooth1 Ψ ε x = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right
𝕂 : 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
⊢ Smooth1 Ψ ε x = 0
Tactic:
unfold Smooth1 MellinConvolution
Proof state after:
case h.right
𝕂 : 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 : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right
𝕂 : 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 : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y = 0
Tactic:
simp only [ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq]
Proof state after:
case h.right
𝕂 : 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 : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right
𝕂 : 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 : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Tactic:
apply setIntegral_eq_zero_of_forall_eq_zero
Proof state after:
case h.right.ht_eq
𝕂 : 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
⊢ ∀ x_1 ∈ Ioi 0, (if 0 < x_1 ∧ x_1 ≤ 1 then DeltaSpike Ψ ε (x / x_1) else 0) / x_1 = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right.ht_eq
𝕂 : 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
⊢ ∀ x_1 ∈ Ioi 0, (if 0 < x_1 ∧ x_1 ≤ 1 then DeltaSpike Ψ ε (x / x_1) else 0) / x_1 = 0
Tactic:
intro y hy
Proof state after:
case h.right.ht_eq
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right.ht_eq
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Tactic:
have ypos := mem_Ioi.mp hy
Proof state after:
case h.right.ht_eq
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Theorem: Smooth1Properties_above
Proof state before:
case h.right.ht_eq
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Tactic:
by_cases y1 : y ≤ 1
Proof state after:
case pos
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0

case neg
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Theorem: Smooth1Properties_above
Proof state before:
case pos
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0

case neg
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Tactic:
swap
Proof state after:
case neg
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0

case pos
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Theorem: Smooth1Properties_above
Proof state before:
case neg
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0

case pos
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Tactic:
simp [ypos, y1]
Proof state after:
case pos
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Theorem: Smooth1Properties_above
Proof state before:
case pos
𝕂 : 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
⊢ (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
Tactic:
simp only [mem_Ioi.mp hy, y1, and_self, ↓reduceIte, div_eq_zero_iff]
Proof state after:
case pos
𝕂 : 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 ∨ y = 0
Theorem: Smooth1Properties_above
Proof state before:
case pos
𝕂 : 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 ∨ y = 0
Tactic:
left
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
⊢ DeltaSpike Ψ ε (x / y) = 0