Theorem: hh'_nonpos (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
⊢ hh' a x ≤ 0
Tactic:
have := pp_pos ha (log x)
State after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ hh' a x ≤ 0

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ hh' a x ≤ 0
Tactic:
simp only [hh', neg_mul, Left.neg_nonpos_iff, ge_iff_le]
State after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ 0 ≤ pp a x.log * hh a x ^ 2

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ 0 ≤ pp a x.log * hh a x ^ 2
Tactic:
positivity
State after:
no goals