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‖ * (C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n)
Tactic:
apply dirichlet_test'
Proof state after:
case ha
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)⁻¹
⊢ 0 ≤ fun n => ‖f n‖

case hb
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)⁻¹
⊢ 0 ≤ fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n

case hAb
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)⁻¹
⊢ atTop.BoundedAtFilter (shift (cumsum fun n => ‖f n‖) * fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n)

case hbb
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)⁻¹
⊢ ∀ᶠ (n : ℕ) in atTop,
    C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n

case h
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 (shift (cumsum fun n => ‖f n‖) * nnabla fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n)