internlm/Lean-Github huggingface dataset:
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 ≤ C * ((2 * π) ^ 2 + (↑n / x).log ^ 2)
Tactic:
gcongr
Proof state after:
case hfg.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
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ (2 * π) ^ 2 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
Theorem: limiting_fourier_lim1_aux
Proof state before:
case hfg.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
n : ℕ
this : 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
⊢ (2 * π) ^ 2 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
Tactic:
apply le_add_of_le_of_nonneg le_rfl (sq_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
n : ℕ
⊢ 0 ≤ (2 * π) ^ 2 + (↑n / x).log ^ 2
Tactic:
positivity
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)
⊢ a =O[atTop] fun n => 1 / ↑n
Tactic:
simpa [a] using IsBigO.mul l5 (isBigO_refl (fun n : ℕ => 1 / (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 𝕜
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
⊢ nnabla a =O[atTop] fun n => (↑n ^ 2 * (↑n).log ^ 2)⁻¹
Tactic:
convert (nnabla_bound C hx).natCast
Proof state after:
case h.e'_7.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
x✝ : ℕ
⊢ nnabla a x✝ = nnabla (fun n => C / (1 + ((n / x).log / (2 * π)) ^ 2) / n) ↑x✝
Theorem: limiting_fourier_lim1_aux
Proof state before:
case h.e'_7.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
x✝ : ℕ
⊢ nnabla a x✝ = nnabla (fun n => C / (1 + ((n / x).log / (2 * π)) ^ 2) / n) ↑x✝
Tactic:
simp [nnabla, a]
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
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‖
Tactic:
intro n
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)⁻¹
n : ℕ
⊢ 0 n ≤ (fun n => ‖f n‖) n
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
n : ℕ
⊢ 0 n ≤ (fun n => ‖f n‖) n
Tactic:
exact norm_nonneg _
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
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
Tactic:
intro n
Proof state after:
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)⁻¹
n : ℕ
⊢ 0 n ≤ (fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n) n
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
n : ℕ
⊢ 0 n ≤ (fun n => C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n) n
Tactic:
positivity
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)
Tactic:
apply (l2.mul l3).trans_eventuallyEq
Proof state after:
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)⁻¹
⊢ (fun x => ↑x * (1 / ↑x)) =ᶠ[atTop] 1
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
⊢ (fun x => ↑x * (1 / ↑x)) =ᶠ[atTop] 1
Tactic:
apply eventually_of_mem (Ici_mem_atTop 1)
Proof state after:
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)⁻¹
⊢ ∀ x ∈ Ici 1, (fun x => ↑x * (1 / ↑x)) x = 1 x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
⊢ ∀ x ∈ Ici 1, (fun x => ↑x * (1 / ↑x)) x = 1 x
Tactic:
intro x (hx : 1 ≤ x)
Proof state after:
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)⁻¹
x : ℕ
hx : 1 ≤ x
⊢ (fun x => ↑x * (1 / ↑x)) x = 1 x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
x : ℕ
hx : 1 ≤ x
⊢ (fun x => ↑x * (1 / ↑x)) x = 1 x
Tactic:
have : x ≠ 0 := by linarith
Proof state after:
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)⁻¹
x : ℕ
hx : 1 ≤ x
this : x ≠ 0
⊢ (fun x => ↑x * (1 / ↑x)) x = 1 x
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
x : ℕ
hx : 1 ≤ x
this : x ≠ 0
⊢ (fun x => ↑x * (1 / ↑x)) x = 1 x
Tactic:
simp [this]
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 : 1 ≤ x
⊢ x ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: limiting_fourier_lim1_aux
Proof state before:
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
Tactic:
have : ∀ᶠ n : ℕ in atTop, x ≤ n := by simpa using eventually_ge_atTop ⌈x⌉₊
Proof state after:
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
⊢ ∀ᶠ (n : ℕ) in atTop,
    C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
Theorem: limiting_fourier_lim1_aux
Proof state before:
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
⊢ ∀ᶠ (n : ℕ) in atTop,
    C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
Tactic:
filter_upwards [this] with n hn
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
Tactic:
have e1 : 0 < (n : ℝ) := by 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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
Tactic:
have e2 : 1 ≤ n / x := (one_le_div (by linarith)).mpr hn
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
e2 : 1 ≤ ↑n / x
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
e2 : 1 ≤ ↑n / x
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
Tactic:
have e3 := Nat.le_succ n
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
e2 : 1 ≤ ↑n / x
e3 : n ≤ n.succ
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
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)⁻¹
this : ∀ᶠ (n : ℕ) in atTop, x ≤ ↑n
n : ℕ
hn : x ≤ ↑n
e1 : 0 < ↑n
e2 : 1 ≤ ↑n / x
e3 : n ≤ n.succ
⊢ C / (1 + ((↑(n + 1) / x).log / (2 * π)) ^ 2) / ↑(n + 1) ≤ C / (1 + ((↑n / x).log / (2 * π)) ^ 2) / ↑n
Tactic:
gcongr
Proof state after:
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 * π)