internlm/Lean-Github huggingface dataset:
Theorem: bound_sum_log
Proof state before:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ 0 ≤ x⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ u / x ∈ Ioi 0
Tactic:
simp
Proof state after:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ 0 < u / x
Theorem: bound_sum_log
Proof state before:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ 0 < u / x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ v / x ∈ Ioi 0
Tactic:
simp
Proof state after:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ 0 < v / x
Theorem: bound_sum_log
Proof state before:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ 0 < v / x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
n : ℕ
u : ℝ
hu1 : 0 < u
right✝¹ : u ≤ ↑n
v : ℝ
hv1 : 0 < v
right✝ : v ≤ ↑n
huv : u ≤ v
⊢ 0 < x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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)
n : ℕ
⊢ IntegrableOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 ↑n) volume
Tactic:
apply IntegrableOn.mono_set (hh_integrable (by positivity) (by positivity) (by positivity)) Icc_subset_Ici_self
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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)
n : ℕ
⊢ 0 < x⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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)
n : ℕ
⊢ 0 < π⁻¹ * 2⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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)
n : ℕ
⊢ 0 < x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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 : ℕ
⊢ 0 ≤ ‖f n‖ / ↑n * (1 + (1 / (2 * π) * (↑n / x).log) ^ 2)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
case h.e'_3
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 : ℕ
⊢ ∑ i ∈ Finset.range n, ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ∑ i ∈ Finset.range n, ‖f i‖ * ggg i
Tactic:
congr
Proof state after:
case h.e'_3.e_f
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 : ℕ
⊢ (fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) = fun i => ‖f i‖ * ggg i
Theorem: bound_sum_log
Proof state before:
case h.e'_3.e_f
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 : ℕ
⊢ (fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) = fun i => ‖f i‖ * ggg i
Tactic:
ext i
Proof state after:
case h.e'_3.e_f.h
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 i : ℕ
⊢ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ‖f i‖ * ggg i
Theorem: bound_sum_log
Proof state before:
case h.e'_3.e_f.h
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 i : ℕ
⊢ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ‖f i‖ * ggg i
Tactic:
by_cases hi : i = 0
Proof state after:
case pos
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 i : ℕ
hi : i = 0
⊢ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ‖f i‖ * ggg i

case neg
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 i : ℕ
hi : ¬i = 0
⊢ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ‖f i‖ * ggg i
Theorem: bound_sum_log
Proof state before:
case pos
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 i : ℕ
hi : i = 0
⊢ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ‖f i‖ * ggg i
Tactic:
simp [hi, hf0]
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
case neg
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 i : ℕ
hi : ¬i = 0
⊢ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ = ‖f i‖ * ggg i
Tactic:
field_simp [hi, ggg, gg]
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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 : ℕ
⊢ ‖f 0‖ = 0
Tactic:
simp [hf0]
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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 : ¬n = 0
⊢ 0 < n
Tactic:
omega
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
⊢ Finset.range n = {0} ∪ Finset.Ico 1 n
Tactic:
ext i
Proof state after:
case a
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
i : ℕ
⊢ i ∈ Finset.range n ↔ i ∈ {0} ∪ Finset.Ico 1 n
Theorem: bound_sum_log
Proof state before:
case a
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
i : ℕ
⊢ i ∈ Finset.range n ↔ i ∈ {0} ∪ Finset.Ico 1 n
Tactic:
simp
Proof state after:
case a
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
i : ℕ
⊢ i < n ↔ i = 0 ∨ 1 ≤ i ∧ i < n
Theorem: bound_sum_log
Proof state before:
case a
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
i : ℕ
⊢ i < n ↔ i = 0 ∨ 1 ≤ i ∧ i < n
Tactic:
by_cases hi : i = 0 <;> simp [hi, hn]
Proof state after:
case neg
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
i : ℕ
hi : ¬i = 0
⊢ i < n → 1 ≤ i
Theorem: bound_sum_log
Proof state before:
case neg
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
i : ℕ
hi : ¬i = 0
⊢ i < n → 1 ≤ i
Tactic:
omega
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
case h.e'_3
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
⊢ (∑ x_1 ∈ Finset.Ico 1 n, if x_1 = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑x_1 / x)) =
    ∑ x_1 ∈ Finset.Ico 1 n, x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑x_1 / x)
Tactic:
apply Finset.sum_congr rfl (fun i hi => ?_)
Proof state after:
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
i : ℕ
hi : i ∈ Finset.Ico 1 n
⊢ (if i = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)) = x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)
Theorem: bound_sum_log
Proof state before:
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
i : ℕ
hi : i ∈ Finset.Ico 1 n
⊢ (if i = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)) = x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)
Tactic:
simp at hi
Proof state after:
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
i : ℕ
hi : 1 ≤ i ∧ i < n
⊢ (if i = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)) = x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)
Theorem: bound_sum_log
Proof state before:
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
i : ℕ
hi : 1 ≤ i ∧ i < n
⊢ (if i = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)) = x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)
Tactic:
have : i ≠ 0 := by omega
Proof state after:
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
i : ℕ
hi : 1 ≤ i ∧ i < n
this : i ≠ 0
⊢ (if i = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)) = x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)
Theorem: bound_sum_log
Proof state before:
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
i : ℕ
hi : 1 ≤ i ∧ i < n
this : i ≠ 0
⊢ (if i = 0 then 1 else x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)) = x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑i / x)
Tactic:
simp [this]
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
i : ℕ
hi : 1 ≤ i ∧ i < n
⊢ i ≠ 0
Tactic:
omega
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
⊢ AntitoneOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Ioc 0 (0 + ↑(n - 1)))
Tactic:
simpa using l5
Proof state after:
no goals