internlm/Lean-Github huggingface dataset:
Theorem: limiting_fourier_lim1_aux
Proof state before:
case h.hac.h.bc.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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
e2 : 1 ≤ ↑n / x
e3 : n ≤ n.succ
⊢ 0 ≤ (↑n / x).log / (2 * π)
Tactic:
refine div_nonneg (Real.log_nonneg e2) (by norm_num [pi_nonneg])
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
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, x ≤ ↑n
Tactic:
simpa using eventually_ge_atTop ⌈x⌉₊
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
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
⊢ 0 < ↑n
Tactic:
linarith
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
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
⊢ 0 < x
Tactic:
linarith
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
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
e2 : 1 ≤ ↑n / x
e3 : n ≤ n.succ
⊢ 0 ≤ 2 * π
Tactic:
norm_num [pi_nonneg]
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)
Tactic:
apply summable_of_isBigO_nat summable_inv_mul_log_sq
Proof state after:
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)⁻¹
⊢ (shift (cumsum fun n => ‖f n‖) * nnabla fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n) =O[atTop] fun n =>
    (↑n * (↑n).log ^ 2)⁻¹
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
⊢ (shift (cumsum fun n => ‖f n‖) * nnabla fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n) =O[atTop] fun n =>
    (↑n * (↑n).log ^ 2)⁻¹
Tactic:
apply (l2.mul l4).trans_eventuallyEq
Proof state after:
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)⁻¹
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) =ᶠ[atTop] fun n => (↑n * (↑n).log ^ 2)⁻¹
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) =ᶠ[atTop] fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
apply eventually_of_mem (Ici_mem_atTop 2)
Proof state after:
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)⁻¹
⊢ ∀ x ∈ Ici 2, (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
⊢ ∀ x ∈ Ici 2, (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Tactic:
intro x (hx : 2 ≤ x)
Proof state after:
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)⁻¹
x : ℕ
hx : 2 ≤ x
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
x : ℕ
hx : 2 ≤ x
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Tactic:
have : (x : ℝ) ≠ 0 := by simp ; linarith
Proof state after:
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Tactic:
have : Real.log x ≠ 0 := by
  have ll : 2 ≤ (x : ℝ) := by simp [hx]
  simp only [ne_eq, log_eq_zero]
  push_neg
  refine ⟨this, ?_, ?_⟩ <;> linarith
Proof state after:
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)⁻¹
x : ℕ
hx : 2 ≤ x
this✝ : ↑x ≠ 0
this : (↑x).log ≠ 0
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
x : ℕ
hx : 2 ≤ x
this✝ : ↑x ≠ 0
this : (↑x).log ≠ 0
⊢ (fun x => ↑x * (↑x ^ 2 * (↑x).log ^ 2)⁻¹) x = (fun n => (↑n * (↑n).log ^ 2)⁻¹) x
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 𝕜
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)⁻¹
x : ℕ
hx : 2 ≤ x
this✝ : ↑x ≠ 0
this : (↑x).log ≠ 0
⊢ ↑x * (↑x * (↑x).log ^ 2) = ↑x ^ 2 * (↑x).log ^ 2
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
x : ℕ
hx : 2 ≤ x
this✝ : ↑x ≠ 0
this : (↑x).log ≠ 0
⊢ ↑x * (↑x * (↑x).log ^ 2) = ↑x ^ 2 * (↑x).log ^ 2
Tactic:
ring
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
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)⁻¹
x : ℕ
hx : 2 ≤ x
⊢ ↑x ≠ 0
Tactic:
simp
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)⁻¹
x : ℕ
hx : 2 ≤ x
⊢ ¬x = 0
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)⁻¹
x : ℕ
hx : 2 ≤ x
⊢ ¬x = 0
Tactic:
linarith
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
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
⊢ (↑x).log ≠ 0
Tactic:
have ll : 2 ≤ (x : ℝ) := by simp [hx]
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
ll : 2 ≤ ↑x
⊢ (↑x).log ≠ 0
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
ll : 2 ≤ ↑x
⊢ (↑x).log ≠ 0
Tactic:
simp only [ne_eq, log_eq_zero]
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
ll : 2 ≤ ↑x
⊢ ¬(↑x = 0 ∨ ↑x = 1 ∨ ↑x = -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
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
ll : 2 ≤ ↑x
⊢ ¬(↑x = 0 ∨ ↑x = 1 ∨ ↑x = -1)
Tactic:
push_neg
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
ll : 2 ≤ ↑x
⊢ ↑x ≠ 0 ∧ ↑x ≠ 1 ∧ ↑x ≠ -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
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
ll : 2 ≤ ↑x
⊢ ↑x ≠ 0 ∧ ↑x ≠ 1 ∧ ↑x ≠ -1
Tactic:
refine ⟨this, ?_, ?_⟩ <;> linarith
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
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)⁻¹
x : ℕ
hx : 2 ≤ x
this : ↑x ≠ 0
⊢ 2 ≤ ↑x
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Tactic:
obtain ⟨C, hC⟩ := decay_bounds_cor ψ
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Theorem: limiting_fourier_lim1
Proof state before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Tactic:
have : 0 ≤ C := by simpa using (norm_nonneg _).trans (hC 0)
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))