Theorem: bound_sum_log0 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
let f0 i := if i = 0 then 0 else f i
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l1 : chebyWith C f0 := by
  intro n ; refine Finset.sum_le_sum (fun i _ => ?_) |>.trans (hf n)
  by_cases hi : i = 0 <;> simp [hi, f0]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l2 i : ‖f i‖ / i = ‖f0 i‖ / i := by by_cases hi : i = 0 <;> simp [hi, f0]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
l2 : ∀ (i : ℕ), ‖f i‖ / ↑i = ‖f0 i‖ / ↑i
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
l2 : ∀ (i : ℕ), ‖f i‖ / ↑i = ‖f0 i‖ / ↑i
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
simp_rw [l2]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
l2 : ∀ (i : ℕ), ‖f i‖ / ↑i = ‖f0 i‖ / ↑i
⊢ ∑' (i : ℕ), ‖f0 i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
l2 : ∀ (i : ℕ), ‖f i‖ / ↑i = ‖f0 i‖ / ↑i
⊢ ∑' (i : ℕ), ‖f0 i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
apply bound_sum_log rfl l1 hx
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
⊢ chebyWith C f0
Tactic:
intro n
State after:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
n : ℕ
⊢ cumsum (fun x => ‖f0 x‖) n ≤ C * ↑n

State before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
n : ℕ
⊢ cumsum (fun x => ‖f0 x‖) n ≤ C * ↑n
Tactic:
refine Finset.sum_le_sum (fun i _ => ?_) |>.trans (hf n)
State after:
n✝ : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
n i : ℕ
x✝ : i ∈ Finset.range n
⊢ (fun x => ‖f0 x‖) i ≤ (fun x => ‖f x‖) i

State before:
n✝ : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
n i : ℕ
x✝ : i ∈ Finset.range n
⊢ (fun x => ‖f0 x‖) i ≤ (fun x => ‖f x‖) i
Tactic:
by_cases hi : i = 0 <;> simp [hi, f0]
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
l1 : chebyWith C f0
i : ℕ
⊢ ‖f i‖ / ↑i = ‖f0 i‖ / ↑i
Tactic:
by_cases hi : i = 0 <;> simp [hi, f0]
State after:
no goals