Theorem: Smooth1Properties_above (PrimeNumberTheoremAnd/MellinCalculus.lean)

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
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

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
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

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
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

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
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

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ε
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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]
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

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]
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

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
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

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Ψ
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

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]
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

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
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

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 : ℝ) ^ ε)]
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

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
State after:
no goals

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]
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

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)
State after:
no goals

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
State after:
no goals

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 : ℝ) ^ ε)]
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
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

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⟩
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

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]
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 / ε)) ^ ε

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
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 / ε)

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
State after:
no goals

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
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

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]
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

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]
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

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
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

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
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

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals