Theorem: hh_le (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
⊢ |hh a t| ≤ t⁻¹
Tactic:
by_cases h0 : t = 0
State after:
case pos
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : t = 0
⊢ |hh a t| ≤ t⁻¹

case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹

State before:
case pos
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : t = 0
⊢ |hh a t| ≤ t⁻¹

case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹
Tactic:
simp [hh, h0]
State after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹

State before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ |hh a t| ≤ t⁻¹
Tactic:
replace ht : 0 < t := lt_of_le_of_ne ht (by tauto)
State after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |hh a t| ≤ t⁻¹

State before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |hh a t| ≤ t⁻¹
Tactic:
unfold hh
State after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |(t * (1 + (a * t.log) ^ 2))⁻¹| ≤ t⁻¹

State before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |(t * (1 + (a * t.log) ^ 2))⁻¹| ≤ t⁻¹
Tactic:
rw [abs_inv, inv_le_inv (by positivity) ht, abs_mul, abs_eq_self.mpr ht.le]
State after:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t ≤ t * |1 + (a * t.log) ^ 2|

State before:
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t ≤ t * |1 + (a * t.log) ^ 2|
Tactic:
convert_to t * 1 ≤ _
State after:
case h.e'_3
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t = t * 1

case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|

State before:
case h.e'_3
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t = t * 1

case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|
Tactic:
simp
State after:
case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|

State before:
case neg.convert_2
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t * 1 ≤ t * |1 + (a * t.log) ^ 2|
Tactic:
apply mul_le_mul le_rfl ?_ zero_le_one ht.le
State after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ |1 + (a * t.log) ^ 2|

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ |1 + (a * t.log) ^ 2|
Tactic:
rw [abs_eq_self.mpr (by positivity)]
State after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ 1 + (a * t.log) ^ 2

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 1 ≤ 1 + (a * t.log) ^ 2
Tactic:
simp
State after:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 ≤ (a * t.log) ^ 2

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 ≤ (a * t.log) ^ 2
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : 0 ≤ t
h0 : ¬t = 0
⊢ 0 ≠ t
Tactic:
tauto
State after:
no goals

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 < |t * (1 + (a * t.log) ^ 2)|
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ 0 ≤ 1 + (a * t.log) ^ 2
Tactic:
positivity
State after:
no goals