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
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
⊢ IntegrableOn (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 (0 + ↑(n - 1))) volume
Tactic:
simpa using l6
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
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)
⊢ 0 ≤ ↑(n - 1) / x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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)
Tactic:
apply Measure.restrict_mono Ioc_subset_Ioi_self le_rfl
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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
Tactic:
apply eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi)
Proof state after:
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
⊢ ∀ x ∈ Ioi 0, 0 x ≤ (fun a => hh (π⁻¹ * 2⁻¹) a) x
Theorem: bound_sum_log
Proof state before:
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
⊢ ∀ x ∈ Ioi 0, 0 x ≤ (fun a => hh (π⁻¹ * 2⁻¹) a) x
Tactic:
intro x (hx : 0 < x)
Proof state after:
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 ∈ Finset.range (n - 1), x✝⁻¹ * hh (π⁻¹ * 2⁻¹) (↑(x + 1) / x✝) ≤
    ∫ (x : ℝ) in 0 ..↑(n - 1), x✝⁻¹ * hh (π⁻¹ * 2⁻¹) (x / x✝)
this : 0 ≤ ↑(n - 1) / x✝
x : ℝ
hx : 0 < x
⊢ 0 x ≤ (fun a => hh (π⁻¹ * 2⁻¹) a) x
Theorem: bound_sum_log
Proof state before:
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 ∈ Finset.range (n - 1), x✝⁻¹ * hh (π⁻¹ * 2⁻¹) (↑(x + 1) / x✝) ≤
    ∫ (x : ℝ) in 0 ..↑(n - 1), x✝⁻¹ * hh (π⁻¹ * 2⁻¹) (x / x✝)
this : 0 ≤ ↑(n - 1) / x✝
x : ℝ
hx : 0 < x
⊢ 0 x ≤ (fun a => hh (π⁻¹ * 2⁻¹) a) x
Tactic:
apply hh_nonneg _ hx.le
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
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))
Tactic:
have := (@hh_integrable 1 (1 / (2 * π)) 1 (by positivity) (by positivity) (by positivity))
Proof state after:
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
this : IntegrableOn (fun t => 1 * hh (1 / (2 * π)) (t / 1)) (Ici 0) volume
⊢ Integrable (fun a => hh (π⁻¹ * 2⁻¹) a) (volume.restrict (Ioi 0))
Theorem: bound_sum_log
Proof state before:
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
this : IntegrableOn (fun t => 1 * hh (1 / (2 * π)) (t / 1)) (Ici 0) volume
⊢ Integrable (fun a => hh (π⁻¹ * 2⁻¹) a) (volume.restrict (Ioi 0))
Tactic:
simpa using this.mono_set Ioi_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)
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 < 1
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 : ℕ
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 < 1 / (2 * π)
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log0
Proof 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
Proof 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)
Theorem: bound_sum_log0
Proof 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]
Proof 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)
Theorem: bound_sum_log0
Proof 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]
Proof 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)
Theorem: bound_sum_log0
Proof 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]
Proof 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)
Theorem: bound_sum_log0
Proof 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
Proof state after:
no goals
Theorem: bound_sum_log0
Proof 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
Proof 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
Theorem: bound_sum_log0
Proof 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)
Proof 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
Theorem: bound_sum_log0
Proof 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]
Proof state after:
no goals
Theorem: bound_sum_log0
Proof 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]
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 : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + 2 * π ^ 2)
Tactic:
simpa only [hh_integral'] using bound_sum_log0 hf hx
Proof state after:
no goals
Theorem: summable_fourier
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
⊢ Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
Tactic:
have l5 : Summable fun i ↦ ‖f i‖ / ↑i * ((1 + (1 / (2 * ↑π) * ↑(Real.log (↑i / x))) ^ 2)⁻¹) := by
  simpa using limiting_fourier_lim1_aux hcheby hx 1 zero_le_one
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
⊢ Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
Theorem: summable_fourier
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
⊢ Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
Tactic:
exact Summable.of_nonneg_of_le (fun _ => norm_nonneg _) l6 (by simpa using l5.const_smul (W21.norm ψ))
Proof state after:
no goals
Theorem: summable_fourier
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
⊢ Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
simpa using limiting_fourier_lim1_aux hcheby hx 1 zero_le_one
Proof state after:
no goals
Theorem: summable_fourier
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
    W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
convert mul_le_mul_of_nonneg_left (decay_bounds_key ψ (1 / (2 * π) * log (i / x))) (norm_nonneg (f i / i)) using 1
Proof state after:
case h.e'_3
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ = ‖f i / ↑i‖ * ‖𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖

case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (‖ψ‖ * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Theorem: summable_fourier
Proof state before:
case h.e'_3
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ = ‖f i / ↑i‖ * ‖𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
Tactic:
simp [norm_mul]
Proof state after:
no goals
Theorem: summable_fourier
Proof state before:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (‖ψ‖ * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
change _ = _ * (W21.norm ψ * _)
Proof state after:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (W21.norm ψ.toFun * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Theorem: summable_fourier
Proof state before:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (W21.norm ψ.toFun * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
simp [W21.norm]
Proof state after:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
      (Complex.abs (f i) / ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹) =
    Complex.abs (f i) / ↑i *
      (((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
        (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹)
Theorem: summable_fourier
Proof state before:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
      (Complex.abs (f i) / ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹) =
    Complex.abs (f i) / ↑i *
      (((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
        (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹)
Tactic:
ring
Proof state after:
no goals
Theorem: summable_fourier
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
⊢ Summable fun b => W21.norm ψ.toFun * (‖f b‖ / ↑b * (1 + (1 / (2 * π) * (↑b / x).log) ^ 2)⁻¹)
Tactic:
simpa using l5.const_smul (W21.norm ψ)
Proof state after:
no goals