internlm/Lean-Github huggingface dataset:
Theorem: hh_integrable_aux
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
⊢ ∫ (t : ℝ) in Ioi 0, a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹ = a * c / b * π
Tactic:
have := integral_Ioi_of_hasDerivAt_of_nonneg k3 key k4 k1
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, g' x = a * c / b * (π / 2) - g₀ 0
⊢ ∫ (t : ℝ) in Ioi 0, a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹ = a * c / b * π
Theorem: hh_integrable_aux
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, g' x = a * c / b * (π / 2) - g₀ 0
⊢ ∫ (t : ℝ) in Ioi 0, a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹ = a * c / b * π
Tactic:
simp only [mul_inv_rev, inv_div, mul_neg, ↓reduceIte, sub_neg_eq_add, g', g₀] at this ⊢
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x)) = a * c / b * (π / 2) + a * c / b * (π / 2)
⊢ ∫ (t : ℝ) in Ioi 0, a * ((1 + (b * (t / c).log) ^ 2)⁻¹ * (c / t)) = a * c / b * π
Theorem: hh_integrable_aux
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x)) = a * c / b * (π / 2) + a * c / b * (π / 2)
⊢ ∫ (t : ℝ) in Ioi 0, a * ((1 + (b * (t / c).log) ^ 2)⁻¹ * (c / t)) = a * c / b * π
Tactic:
convert this 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 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x)) = a * c / b * (π / 2) + a * c / b * (π / 2)
⊢ a * c / b * π = a * c / b * (π / 2) + a * c / b * (π / 2)
Theorem: hh_integrable_aux
Proof state before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x)) = a * c / b * (π / 2) + a * c / b * (π / 2)
⊢ a * c / b * π = a * c / b * (π / 2) + a * c / b * (π / 2)
Tactic:
field_simp
Proof state after:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x)) = a * c / b * (π / 2) + a * c / b * (π / 2)
⊢ a * c * π * (b * 2) = (a * c * π + a * c * π) * b
Theorem: hh_integrable_aux
Proof state before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
this : ∫ (x : ℝ) in Ioi 0, a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x)) = a * c / b * (π / 2) + a * c / b * (π / 2)
⊢ a * c * π * (b * 2) = (a * c * π + a * c * π) * b
Tactic:
ring
Proof state after:
no goals
Theorem: hh_integral'
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t = 2 * π ^ 2
Tactic:
have := hh_integral (a := 1) (b := 1 / (2 * π)) (c := 1) (by positivity) (by positivity) (by positivity)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t = 2 * π ^ 2
Theorem: hh_integral'
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t = 2 * π ^ 2
Tactic:
convert this using 1 <;> simp
Proof state after:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ 2 * π ^ 2 = 2 * π * π
Theorem: hh_integral'
Proof state before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ 2 * π ^ 2 = 2 * π * π
Tactic:
ring
Proof state after:
no goals
Theorem: hh_integral'
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_integral'
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1 / (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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
let ggg (i : ℕ) : ℝ := if i = 0 then 1 else gg x i
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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l0 : x ≠ 0 := by linarith
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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
l0 : x ≠ 0
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l1 i : 0 ≤ ggg i := by by_cases hi : i = 0 <;> simp [ggg, hi, gg] ; 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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l3 : 0 ≤ C := by simpa [cumsum, hf0] using hf 1
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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
l3 : 0 ≤ C
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t :=
  setIntegral_nonneg measurableSet_Ioi (fun x hx => hh_nonneg _ (LT.lt.le hx))
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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
l2 : Antitone ggg
l3 : 0 ≤ C
l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l5 {n : ℕ} : AntitoneOn (fun t ↦ x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 n) := by
  intro u ⟨hu1, _⟩ v ⟨hv1, _⟩ huv
  simp only
  apply mul_le_mul le_rfl ?_ (hh_nonneg _ (by positivity)) (by positivity)
  apply hh_antitone one_div_two_pi_mem_Ioo (by simp ; positivity) (by simp ; positivity)
  apply (div_le_div_right (by positivity)).mpr 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
l5 : ∀ {n : ℕ}, AntitoneOn (fun t => x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 ↑n)
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
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)
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
have l6 {n : ℕ} : IntegrableOn (fun t ↦ x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 n) volume := by
  apply IntegrableOn.mono_set (hh_integrable (by positivity) (by positivity) (by positivity)) Icc_subset_Ici_self
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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
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
⊢ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
apply Real.tsum_le_of_sum_range_le (fun n => 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
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)⁻¹ ≤
      C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
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)⁻¹ ≤
      C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
intro n
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 : ℕ
⊢ ∑ i ∈ Finset.range n, ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (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
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)⁻¹ ≤
    C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)
Tactic:
convert_to ∑ i in Finset.range n, ‖f i‖ * ggg i ≤ _
Proof state after:
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

case 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 : ℕ
⊢ ∑ i ∈ Finset.range n, ‖f i‖ * ggg i ≤ C * (1 + ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t)