Theorem: bound_main (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))
Tactic:
have l1 := bound_I1' x hx ψ hcheby
State after:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))

State before:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))
Tactic:
have l2 := mul_le_mul (le_refl ‖A‖) (bound_I2 x ψ) (by positivity) (by positivity)
State after:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
l2 : ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))

State before:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
l2 : ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))
Tactic:
apply norm_sub_le _ _ |>.trans
State after:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
l2 : ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ +
      ‖A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))

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

State before:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
l2 : ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ +
      ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2))
Tactic:
convert _root_.add_le_add l1 l2 using 1
State after:
case h.e'_4
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
l2 : ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
⊢ W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2)) =
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2) + ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))

State before:
case h.e'_4
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
l2 : ‖A‖ * ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
⊢ W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2) + ‖A‖ * (2 * π ^ 2)) =
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2) + ‖A‖ * (W21.norm ψ.toFun * (2 * π ^ 2))
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A✝ a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
⊢ 0 ≤ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (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 𝕜
C : ℝ
A : ℂ
x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
l1 : ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
⊢ 0 ≤ ‖A‖
Tactic:
positivity
State after:
no goals