Theorem: bound_sum_log
Proof state before:
case neg.convert_2
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf0 : f 0 = 0
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
ggg : ℕ → ℝ := fun i => if i = 0 then 1 else gg x ↑i
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
l3 : 0 ≤ C
l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
l5 : ∀ {n : ℕ}, AntitoneOn (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 ↑n)
l6 : ∀ {n : ℕ}, IntegrableOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 ↑n) volume
n : ℕ
hn : 0 < n
this✝¹ : Finset.range n = {0} ∪ Finset.Ico 1 n
this✝ :
  ∑ x_1 ∈ Finset.range (n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑(x_1 + 1) / x) ≤
    ∫ (x_1 : ℝ) in 0 ..↑(n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (x_1 / x)
this : 0 ≤ ↑(n - 1) / x
⊢ ∫ (x : ℝ) in Ioc 0 (↑(n - 1) / x), hh (π⁻¹ * 2⁻¹) x ∂volume ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
Tactic:
apply integral_mono_measure
Proof state after:
case neg.convert_2.hle
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf0 : f 0 = 0
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
ggg : ℕ → ℝ := fun i => if i = 0 then 1 else gg x ↑i
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
l3 : 0 ≤ C
l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
l5 : ∀ {n : ℕ}, AntitoneOn (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 ↑n)
l6 : ∀ {n : ℕ}, IntegrableOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 ↑n) volume
n : ℕ
hn : 0 < n
this✝¹ : Finset.range n = {0} ∪ Finset.Ico 1 n
this✝ :
  ∑ x_1 ∈ Finset.range (n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑(x_1 + 1) / x) ≤
    ∫ (x_1 : ℝ) in 0 ..↑(n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (x_1 / x)
this : 0 ≤ ↑(n - 1) / x
⊢ volume.restrict (Ioc 0 (↑(n - 1) / x)) ≤ volume.restrict (Ioi 0)

case neg.convert_2.hf
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf0 : f 0 = 0
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
ggg : ℕ → ℝ := fun i => if i = 0 then 1 else gg x ↑i
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
l3 : 0 ≤ C
l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
l5 : ∀ {n : ℕ}, AntitoneOn (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 ↑n)
l6 : ∀ {n : ℕ}, IntegrableOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 ↑n) volume
n : ℕ
hn : 0 < n
this✝¹ : Finset.range n = {0} ∪ Finset.Ico 1 n
this✝ :
  ∑ x_1 ∈ Finset.range (n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑(x_1 + 1) / x) ≤
    ∫ (x_1 : ℝ) in 0 ..↑(n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (x_1 / x)
this : 0 ≤ ↑(n - 1) / x
⊢ 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] fun a => hh (π⁻¹ * 2⁻¹) a

case neg.convert_2.hfi
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf0 : f 0 = 0
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
ggg : ℕ → ℝ := fun i => if i = 0 then 1 else gg x ↑i
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
l3 : 0 ≤ C
l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
l5 : ∀ {n : ℕ}, AntitoneOn (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 ↑n)
l6 : ∀ {n : ℕ}, IntegrableOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 ↑n) volume
n : ℕ
hn : 0 < n
this✝¹ : Finset.range n = {0} ∪ Finset.Ico 1 n
this✝ :
  ∑ x_1 ∈ Finset.range (n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑(x_1 + 1) / x) ≤
    ∫ (x_1 : ℝ) in 0 ..↑(n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (x_1 / x)
this : 0 ≤ ↑(n - 1) / x
⊢ Integrable (fun a => hh (π⁻¹ * 2⁻¹) a) (volume.restrict (Ioi 0))