internlm/Lean-Github huggingface dataset:
Theorem: nnabla_bound_aux
Proof state before:
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
e2 : n ≠ 1
⊢ n.log ≠ 0
Tactic:
have e3 : n ≠ -1 := by linarith
Proof state after:
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
e2 : n ≠ 1
e3 : n ≠ -1
⊢ n.log ≠ 0
Theorem: nnabla_bound_aux
Proof state before:
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
e2 : n ≠ 1
e3 : n ≠ -1
⊢ n.log ≠ 0
Tactic:
simp [e1, e2, e3]
Proof state after:
no goals
Theorem: nnabla_bound_aux
Proof state before:
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
⊢ n ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: nnabla_bound_aux
Proof state before:
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
⊢ n ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: nnabla_bound_aux
Proof state before:
n✝ : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l6 : (fun n => d (n + 1) - d n) =O[atTop] fun n => n.log ^ 2
n : ℝ
hn : 2 ≤ n
e1 : n ≠ 0
e2 : n ≠ 1
⊢ n ≠ -1
Tactic:
linarith
Proof state after:
no goals
Theorem: nnabla_bound
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (nnabla fun n => C / (1 + ((n / x).log / (2 * π)) ^ 2) / n) =O[atTop] fun n => (n ^ 2 * n.log ^ 2)⁻¹
Tactic:
field_simp
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (nnabla fun n => C * (2 * π) ^ 2 / (((2 * π) ^ 2 + (n / x).log ^ 2) * n)) =O[atTop] fun n => 1 / (n ^ 2 * n.log ^ 2)
Theorem: nnabla_bound
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (nnabla fun n => C * (2 * π) ^ 2 / (((2 * π) ^ 2 + (n / x).log ^ 2) * n)) =O[atTop] fun n => 1 / (n ^ 2 * n.log ^ 2)
Tactic:
simp [div_eq_mul_inv]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ ((C * (2 * π) ^ 2) • nnabla fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
Theorem: nnabla_bound
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ ((C * (2 * π) ^ 2) • nnabla fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
Tactic:
apply IsBigO.const_mul_left
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) x_1) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
Theorem: nnabla_bound
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) x_1) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
Tactic:
field_simp
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) x_1) =O[atTop] fun n =>
    1 / (n.log ^ 2 * n ^ 2)
Theorem: nnabla_bound
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) x_1) =O[atTop] fun n =>
    1 / (n.log ^ 2 * n ^ 2)
Tactic:
exact nnabla_bound_aux hx
Proof state after:
no goals
Theorem: cheby.bigO
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h : cheby f
l1 : 0 ≤ cumsum fun x => ‖f x‖
⊢ (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
Tactic:
obtain ⟨C, hC⟩ := h
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
Theorem: cheby.bigO
Proof state before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
Tactic:
apply isBigO_of_le' (c := C) atTop
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ ∀ (x : ℕ), ‖cumsum (fun x => ‖f x‖) x‖ ≤ C * ‖↑x‖
Theorem: cheby.bigO
Proof state before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
⊢ ∀ (x : ℕ), ‖cumsum (fun x => ‖f x‖) x‖ ≤ C * ‖↑x‖
Tactic:
intro n
Proof state after:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ ‖cumsum (fun x => ‖f x‖) n‖ ≤ C * ‖↑n‖
Theorem: cheby.bigO
Proof state before:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ ‖cumsum (fun x => ‖f x‖) n‖ ≤ C * ‖↑n‖
Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr (l1 n)]
Proof state after:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ cumsum (fun x => ‖f x‖) n ≤ C * ‖↑n‖
Theorem: cheby.bigO
Proof state before:
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ cumsum (fun x => ‖f x‖) n ≤ C * ‖↑n‖
Tactic:
simpa using hC n
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hx : 0 < x
C : ℝ
hC : 0 ≤ C
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
let a (n : ℕ) := (C / (1 + (Real.log (↑n / x) / (2 * π)) ^ 2) / ↑n)
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
replace hcheby := hcheby.bigO
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
have l5 : BoundedAtFilter atTop (fun n : ℕ => C / (1 + (Real.log (↑n / x) / (2 * π)) ^ 2)) := by
  field_simp [BoundedAtFilter]
  apply isBigO_of_le' (c := C) ; intro n
  have : 0 ≤ (2 * π) ^ 2 + Real.log (n / x) ^ 2 := by positivity
  simp [abs_eq_self.mpr hC, abs_eq_self.mpr pi_nonneg, abs_eq_self.mpr this]
  apply div_le_of_nonneg_of_le_mul this hC
  gcongr
  apply le_add_of_le_of_nonneg le_rfl (sq_nonneg _)
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
have l3 : a =O[atTop] (fun n => 1 / (n : ℝ)) := by
  simpa [a] using IsBigO.mul l5 (isBigO_refl (fun n : ℕ => 1 / (n : ℝ)) _)
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
l3 : a =O[atTop] fun n => 1 / ↑n
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
l3 : a =O[atTop] fun n => 1 / ↑n
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
have l4 : nnabla a =O[atTop] (fun n : ℕ => (n ^ 2 * (Real.log n) ^ 2)⁻¹) := by
  convert (nnabla_bound C hx).natCast ; simp [nnabla, a]
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
l3 : a =O[atTop] fun n => 1 / ↑n
l4 : nnabla a =O[atTop] fun n => (↑n ^ 2 * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
l3 : a =O[atTop] fun n => 1 / ↑n
l4 : nnabla a =O[atTop] fun n => (↑n ^ 2 * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
simp_rw [div_mul_eq_mul_div, mul_div_assoc, one_mul]
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
l5 : atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
l3 : a =O[atTop] fun n => 1 / ↑n
l4 : nnabla a =O[atTop] fun n => (↑n ^ 2 * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => ‖f n‖ * (C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n)
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
⊢ (fun n => ↑(n + 1)) =O[atTop] fun n => ↑n
Tactic:
simpa using (isBigO_refl _ _).add <| isBigO_iff.mpr ⟨1, by simpa using ⟨1, by tauto⟩⟩
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖1‖ ≤ 1 * ‖↑x‖
Tactic:
simpa using ⟨1, by tauto⟩
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
⊢ ∀ (b : ℕ), 1 ≤ b → 1 ≤ b
Tactic:
tauto
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ atTop.BoundedAtFilter fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2)
Tactic:
field_simp [BoundedAtFilter]
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ (fun n => C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)) =O[atTop] 1
Theorem: limiting_fourier_lim1_aux
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ (fun n => C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)) =O[atTop] 1
Tactic:
apply isBigO_of_le' (c := C)
Proof state after:
case hfg
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ ∀ (x_1 : ℕ), ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑x_1 / x).log ^ 2)‖ ≤ C * ‖1 x_1‖
Theorem: limiting_fourier_lim1_aux
Proof state before:
case hfg
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
⊢ ∀ (x_1 : ℕ), ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑x_1 / x).log ^ 2)‖ ≤ C * ‖1 x_1‖
Tactic:
intro n
Proof state after:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
⊢ ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)‖ ≤ C * ‖1 n‖
Theorem: limiting_fourier_lim1_aux
Proof state before:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
⊢ ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)‖ ≤ C * ‖1 n‖
Tactic:
have : 0 ≤ (2 * π) ^ 2 + Real.log (n / x) ^ 2 := by positivity
Proof state after:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)‖ ≤ C * ‖1 n‖
Theorem: limiting_fourier_lim1_aux
Proof state before:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ ‖C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2)‖ ≤ C * ‖1 n‖
Tactic:
simp [abs_eq_self.mpr hC, abs_eq_self.mpr pi_nonneg, abs_eq_self.mpr this]
Proof state after:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2) ≤ C
Theorem: limiting_fourier_lim1_aux
Proof state before:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ C * (2 * π) ^ 2 / ((2 * π) ^ 2 + (↑n / x).log ^ 2) ≤ C
Tactic:
apply div_le_of_nonneg_of_le_mul this hC
Proof state after:
case hfg
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
C : ℝ
hC : 0 ≤ C
a : ℕ → ℝ := fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
hcheby : (cumsum fun x => ‖f x‖) =O[atTop] Nat.cast
l1 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑(n + 1)
l2 : shift (cumsum fun x => ‖f x‖) =O[atTop] fun n => ↑n
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ C * (2 * π) ^ 2 ≤ C * ((2 * π) ^ 2 + (↑n / x).log ^ 2)