Theorem: bound_I1' (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
Tactic:
apply bound_I1 x (by linarith) ψ ⟨_, hcheby⟩ |>.trans
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
Tactic:
rw [smul_eq_mul, mul_assoc]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun * ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2))

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun * ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2))
Tactic:
apply mul_le_mul le_rfl (bound_sum_log' hcheby hx) ?_ W21.norm_nonneg
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ 0 ≤ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ 0 ≤ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
apply tsum_nonneg (fun i => by positivity)
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ 0 < x
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
i : ℕ
⊢ 0 ≤ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
positivity
State after:
no goals