internlm/Lean-Github huggingface dataset:
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)
⊢ ∫ (x_1 : ℝ) in 0 ..↑(n - 1), x⁻¹ * hh (π⁻¹ * 2⁻¹) (x_1 / x) ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
Tactic:
rw [@intervalIntegral.integral_comp_div ℝ _ _ 0 ↑(n - 1) x (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t)) l0]
Proof state after:
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)
⊢ x • ∫ (x_1 : ℝ) in 0 / x..↑(n - 1) / x, x⁻¹ * hh (π⁻¹ * 2⁻¹) x_1 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
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)
⊢ x • ∫ (x_1 : ℝ) in 0 / x..↑(n - 1) / x, x⁻¹ * hh (π⁻¹ * 2⁻¹) x_1 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
Tactic:
simp [← mul_assoc, mul_inv_cancel l0]
Proof state after:
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)
⊢ ∫ (x : ℝ) in 0 ..↑(n - 1) / x, hh (π⁻¹ * 2⁻¹) x ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
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)
⊢ ∫ (x : ℝ) in 0 ..↑(n - 1) / x, hh (π⁻¹ * 2⁻¹) x ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
Tactic:
have : (0 : ℝ) ≤ ↑(n - 1) / x := by positivity
Proof state after:
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 0 ..↑(n - 1) / x, hh (π⁻¹ * 2⁻¹) x ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
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 0 ..↑(n - 1) / x, hh (π⁻¹ * 2⁻¹) x ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
Tactic:
rw [intervalIntegral.intervalIntegral_eq_integral_uIoc]
Proof state after:
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
⊢ (if 0 ≤ ↑(n - 1) / x then 1 else -1) • ∫ (x : ℝ) in Ι 0 (↑(n - 1) / x), hh (π⁻¹ * 2⁻¹) x ∂volume ≤
    ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
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
⊢ (if 0 ≤ ↑(n - 1) / x then 1 else -1) • ∫ (x : ℝ) in Ι 0 (↑(n - 1) / x), hh (π⁻¹ * 2⁻¹) x ∂volume ≤
    ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
Tactic:
simp [this]
Proof state after:
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
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
⊢ x ≠ 0
Tactic:
linarith
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
i : ℕ
⊢ 0 ≤ ggg i
Tactic:
by_cases hi : i = 0 <;> simp [ggg, hi, gg]
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
i : ℕ
hi : ¬i = 0
⊢ 0 ≤ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹
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
i : ℕ
hi : ¬i = 0
⊢ 0 ≤ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 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
⊢ Antitone ggg
Tactic:
intro i j hij
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
i j : ℕ
hij : i ≤ j
⊢ ggg j ≤ ggg i
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
i j : ℕ
hij : i ≤ j
⊢ ggg j ≤ ggg i
Tactic:
by_cases hi : i = 0 <;> by_cases hj : j = 0 <;> simp [ggg, hi, hj]
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
i j : ℕ
hij : i ≤ j
hi : i = 0
hj : ¬j = 0
⊢ gg x ↑j ≤ 1

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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : j = 0
⊢ 1 ≤ gg x ↑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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ gg x ↑j ≤ gg x ↑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
i j : ℕ
hij : i ≤ j
hi : i = 0
hj : ¬j = 0
⊢ gg x ↑j ≤ 1
Tactic:
exact gg_le_one _
Proof state after:
no goals
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : j = 0
⊢ 1 ≤ gg x ↑i
Tactic:
omega
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ gg x ↑j ≤ gg x ↑i
Tactic:
simp only [gg_of_hh l0]
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ x⁻¹ * hh (1 / (2 * π)) (↑j / x) ≤ x⁻¹ * hh (1 / (2 * π)) (↑i / x)
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ x⁻¹ * hh (1 / (2 * π)) (↑j / x) ≤ x⁻¹ * hh (1 / (2 * π)) (↑i / x)
Tactic:
gcongr
Proof state after:
case neg.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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ hh (1 / (2 * π)) (↑j / x) ≤ hh (1 / (2 * π)) (↑i / x)
Theorem: bound_sum_log
Proof state before:
case neg.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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ hh (1 / (2 * π)) (↑j / x) ≤ hh (1 / (2 * π)) (↑i / x)
Tactic:
apply hh_antitone one_div_two_pi_mem_Ioo
Proof state after:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ ↑i / x ∈ Ioi 0

case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ ↑j / x ∈ Ioi 0

case neg.h.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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ ↑i / x ≤ ↑j / x
Theorem: bound_sum_log
Proof state before:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ ↑i / x ∈ Ioi 0
Tactic:
simp
Proof state after:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ 0 < ↑i / x
Theorem: bound_sum_log
Proof state before:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ 0 < ↑i / x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ ↑j / x ∈ Ioi 0
Tactic:
simp
Proof state after:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ 0 < ↑j / x
Theorem: bound_sum_log
Proof state before:
case neg.h.x
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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ 0 < ↑j / x
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_sum_log
Proof state before:
case neg.h.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
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ ↑i / x ≤ ↑j / x
Tactic:
gcongr
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
⊢ 0 ≤ C
Tactic:
simpa [cumsum, hf0] using hf 1
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 : ℕ
⊢ AntitoneOn (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 ↑n)
Tactic:
intro u ⟨hu1, _⟩ v ⟨hv1, _⟩ huv
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
⊢ (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) v ≤ (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) u
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
⊢ (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) v ≤ (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) u
Tactic:
simp only
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
⊢ x⁻¹ * hh (1 / (2 * π)) (v / x) ≤ x⁻¹ * hh (1 / (2 * π)) (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
⊢ x⁻¹ * hh (1 / (2 * π)) (v / x) ≤ x⁻¹ * hh (1 / (2 * π)) (u / x)
Tactic:
apply mul_le_mul le_rfl ?_ (hh_nonneg _ (by positivity)) (by positivity)
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
⊢ hh (1 / (2 * π)) (v / x) ≤ hh (1 / (2 * π)) (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
⊢ hh (1 / (2 * π)) (v / x) ≤ hh (1 / (2 * π)) (u / x)
Tactic:
apply hh_antitone one_div_two_pi_mem_Ioo (by simp ; positivity) (by simp ; positivity)
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
⊢ u / x ≤ 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
⊢ u / x ≤ v / x
Tactic:
apply (div_le_div_right (by positivity)).mpr huv
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 ≤ v / x
Tactic:
positivity
Proof state after:
no goals