Theorem: gg_le_one (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
⊢ gg x ↑i ≤ 1
Tactic:
by_cases hi : i = 0 <;> simp [gg, hi]
State after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1

State before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Tactic:
have l1 : 1 ≤ (i : ℝ) := by simp ; omega
State after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1

State before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Tactic:
have l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * Real.log (↑i / x)) ^ 2 := by simp ; positivity
State after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1

State before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Tactic:
rw [← mul_inv]
State after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2))⁻¹ ≤ 1

State before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2))⁻¹ ≤ 1
Tactic:
apply inv_le_one
State after:
case neg.ha
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 1 ≤ ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)

State before:
case neg.ha
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 1 ≤ ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)
Tactic:
simpa using mul_le_mul l1 l2 zero_le_one (by simp)
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ 1 ≤ ↑i
Tactic:
simp
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ 1 ≤ i

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

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

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ 0 ≤ (π⁻¹ * 2⁻¹ * (↑i / x).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 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 0 ≤ ↑i
Tactic:
simp
State after:
no goals