Theorem: Smooth1Properties_above_aux2 (PrimeNumberTheoremAnd/MellinCalculus.lean)

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

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

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 := ?_
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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