Theorem: Smooth1Properties_above_aux (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε < x
Tactic:
calc
  x ≥ 1 + (2 * Real.log 2) * ε := hx
  _ > 2 ^ ε := ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 1 + 2 * Real.log 2 * ε > 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 1 + 2 * Real.log 2 * ε > 2 ^ ε
Tactic:
refine lt_add_of_sub_left_lt <| (div_lt_iff hε.1).mp ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ ε - 1) / ε < 2 * Real.log 2

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ ε - 1) / ε < 2 * Real.log 2
Tactic:
calc
  2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε := ?_
  _ > 2 ^ ε * (1 - 2 ^ (-ε)) / ε := ?_
  _ = (2 ^ ε - 1) / ε := ?_
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε

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

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Tactic:
have := (mul_lt_mul_left (a := 2) (by norm_num)).mpr <| Smooth1Properties_estimate hε.1
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * ((1 - 2 ^ (-ε)) / ε) < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * ((1 - 2 ^ (-ε)) / ε) < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Tactic:
field_simp at this
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * (1 - 2 ^ (-ε)) / ε < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * (1 - 2 ^ (-ε)) / ε < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Tactic:
simp [this]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Tactic:
have : (2 : ℝ) ^ ε < 2 := by
  nth_rewrite 1 [← pow_one 2]
  convert rpow_lt_rpow_of_exponent_lt (x := 2) (by norm_num) hε.2 <;> norm_num
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
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε

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

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

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 ⊢
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 ^ ε * ε⁻¹

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

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]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ 1) ^ ε < 2

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

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

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
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 ^ (-ε)

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

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

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

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

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

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

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