From 9bbe1ab56acf8cd5ebda1e3863028775fb2508e6 Mon Sep 17 00:00:00 2001 From: teorth Date: Wed, 24 Jan 2024 23:57:12 -0800 Subject: [PATCH 1/2] adding some statements --- PrimeNumberTheoremAnd/Wiener.lean | 45 +++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean index 11341ccd..143a635f 100644 --- a/PrimeNumberTheoremAnd/Wiener.lean +++ b/PrimeNumberTheoremAnd/Wiener.lean @@ -1,4 +1,12 @@ import PrimeNumberTheoremAnd.EulerProducts.PNT +import Mathlib.Analysis.Fourier.FourierTransform +import Mathlib.NumberTheory.ArithmeticFunction +import Mathlib.Topology.Support +import Mathlib.Analysis.Calculus.ContDiff.Defs + +open Nat Real BigOperators +open Complex hiding log +-- can't open ArithmeticFunction because this causes a namespace collision with σ. Couldn't figure out how to use `open hiding` to fix this. /-%% The Fourier transform of an absolutely integrable function $\psi: \R \to \C$ is defined by the formula @@ -8,11 +16,20 @@ where $e(\theta) := e^{2\pi i \theta}$. Let $f: \N \to \C$ be an arithmetic function such that $\sum_{n=1}^\infty \frac{|f(n)|}{n^\sigma} < \infty$ for all $\sigma>1$. Then the Dirichlet series $$ F(s) := \sum_{n=1}^\infty \frac{f(n)}{n^s}$$ is absolutely convergent for $\sigma>1$. +%%-/ +variable {f: ArithmeticFunction ℝ} (hf: ∀ (σ:ℝ), 1 < σ → Summable (fun n ↦ |f n| / n^σ)) + +/-%% \begin{lemma}[First Fourier identity]\label{first-fourier} If $\psi: \R \to \C$ is continuous and compactly supported and $x > 0$, then for any $\sigma>1$ $$ \sum_{n=1}^\infty \frac{f(n)}{n^\sigma} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = \int_\R F(\sigma + it) \psi(t) x^{it}\ dt.$$ \end{lemma} +%%-/ + +lemma first_fourier {ψ:ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompactSupport ψ) {x σ:ℝ} (hx: 0 < x) (hσ: 1 < σ) : ∑' n : ℕ, f n / (n^σ:ℝ) * (fourierIntegral ψ (1 / (2 * π) * log (n / x))) = ∫ t:ℝ, ArithmeticFunction.LSeries f (σ + t * I) * ψ t * x^(t * I) ∂ volume := by + sorry +/-%% \begin{proof} By the definition of the Fourier transform, the left-hand side expands as $$ \sum_{n=1}^\infty \int_\R \frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log \frac{n}{x})\ dt$$ while the right-hand side expands as @@ -21,11 +38,18 @@ Since $$\frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log \frac{n}{x}) = \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it}$$ the claim then follows from Fubini's theorem. \end{proof} +%%-/ +/-%% \begin{lemma}[Second Fourier identity]\label{second-fourier} If $\psi: \R \to \C$ is continuous and compactly supported and $x > 0$, then for any $\sigma>1$ $$ \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du = x^{\sigma - 1} \int_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt.$$ \end{lemma} +%%-/ + +lemma second_fourier {ψ:ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompactSupport ψ) {x σ:ℝ} (hx: 0 < x) (hσ: 1 < σ) : ∫ u in Set.Ici (-log x), Real.exp (-u * (σ - 1)) * fourierIntegral ψ (u / (2 * π)) = (x^(σ - 1):ℝ) * ∫ t, (1 / (σ + t * I - 1)) * ψ t * x^(t * I) ∂ volume := + sorry +/-%% \begin{proof} \uses{first-fourier} The left-hand side expands as @@ -34,27 +58,48 @@ $$ \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du = x^{\si $$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} e(-\frac{tu}{2\pi})\ du = x^{\sigma - 1} \frac{1}{\sigma+it-1} x^{it}$$ which is a routine calculation. \end{proof} +%%-/ +/-%% Now let $A \in \C$, and suppose that there is a continuous function $G(s)$ defined on $\mathrm{Re} s \geq 1$ such that $G(s) = F(s) - \frac{A}{s-1}$ whenever $\mathrm{Re} s > 1$. We also make the Chebyshev-type hypothesis \begin{equation}\label{cheby} \sum_{n \leq x} |f(n)| \ll x \end{equation} for all $x \geq 1$ (this hypothesis is not strictly necessary, but simplifies the arguments and can be obtained fairly easily in applications). +%%-/ + +variable {A:ℝ} {G:ℂ → ℂ} (hG: ContinuousOn G {s | 1 ≤ s.re}) (hG' : Set.EqOn G (fun s ↦ ArithmeticFunction.LSeries f s - A / (s - 1)) {s | 1 < s.re}) +variable (hcheby: ∃ C:ℝ, ∀ x:ℕ, ∑ n in Finset.Iic x, |f n| ≤ C * x) + +/-%% \begin{lemma}[Decay bounds]\label{decay} If $\psi:\R \to \C$ is $C^2$ and obeys the bounds $$ |\psi(t)|, |\psi''(t)| \leq A / (1 + |t|^2)$$ for all $t \in \R$, then $$ |\hat \psi(u)| \leq C A / (1+|u|^2)$$ for all $u \in \R$, where $C$ is an absolute constant. \end{lemma} +%%-/ + +lemma decay_bounds : ∃ C:ℝ, ∀ (ψ:ℝ → ℂ) (hψ: ContDiff ℝ 2 ψ) (hsupp: HasCompactSupport ψ) (A:ℝ) (hA: ∀ t, ‖ψ t‖ ≤ A / (1 + t^2)) (hA': ∀ t, ‖deriv^[2] ψ t‖ ≤ A / (1 + t^2)) (u:ℝ), ‖fourierIntegral ψ u‖ ≤ C * A / (1 + u^2) := by + sorry +/-%% \begin{proof} This follows from a standard integration by parts argument. \end{proof} +%%-/ +/-%% \begin{lemma}[Limiting Fourier identity]\label{limiting} If $\psi: \R \to \C$ is $C^2$ and compactly supported and $x \geq 1$, then $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) - A \int_{-\log x}^\infty \hat \psi(\frac{u}{2\pi})\ du = \int_\R G(1+it) \psi(t) x^{it}\ dt.$$ \end{lemma} +%%-/ + +lemma limiting_fourier {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasCompactSupport ψ) {x:ℝ} (hx: 1 ≤ x) : ∑' n, f(n) / n * fourierIntegral ψ (1/(2*π) * log (n/x)) - A * ∫ u in Set.Ici (-log x), fourierIntegral ψ (u / (2*π)) ∂ volume = ∫ t, (G (1 + I*t)) * (ψ t) * x^(I * t) ∂ volume := by + sorry + +/-%% \begin{proof} \uses{first-fourier,second-fourier,decay} By the preceding two lemmas, we know that for any $\sigma>1$, we have From 5d9ae620c0f068d7f9db964e61e155b080c71948 Mon Sep 17 00:00:00 2001 From: teorth Date: Thu, 25 Jan 2024 13:14:59 -0800 Subject: [PATCH 2/2] spelling of wiener ikehara lemmas --- PrimeNumberTheoremAnd/Wiener.lean | 57 +++++++++++++++++++++++++++---- 1 file changed, 51 insertions(+), 6 deletions(-) diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean index 143a635f..605725af 100644 --- a/PrimeNumberTheoremAnd/Wiener.lean +++ b/PrimeNumberTheoremAnd/Wiener.lean @@ -4,9 +4,9 @@ import Mathlib.NumberTheory.ArithmeticFunction import Mathlib.Topology.Support import Mathlib.Analysis.Calculus.ContDiff.Defs -open Nat Real BigOperators +open Nat Real BigOperators ArithmeticFunction open Complex hiding log --- can't open ArithmeticFunction because this causes a namespace collision with σ. Couldn't figure out how to use `open hiding` to fix this. +-- note: the opening of ArithmeticFunction introduces a notation σ that seems impossible to hide, and hence parameters that are traditionally called σ will have to be called σ' instead in this file. /-%% The Fourier transform of an absolutely integrable function $\psi: \R \to \C$ is defined by the formula @@ -18,7 +18,7 @@ $$ F(s) := \sum_{n=1}^\infty \frac{f(n)}{n^s}$$ is absolutely convergent for $\sigma>1$. %%-/ -variable {f: ArithmeticFunction ℝ} (hf: ∀ (σ:ℝ), 1 < σ → Summable (fun n ↦ |f n| / n^σ)) +variable {f: ArithmeticFunction ℝ} (hf: ∀ (σ':ℝ), 1 < σ' → Summable (fun n ↦ |f n| / n^σ')) /-%% \begin{lemma}[First Fourier identity]\label{first-fourier} If $\psi: \R \to \C$ is continuous and compactly supported and $x > 0$, then for any $\sigma>1$ @@ -26,7 +26,7 @@ variable {f: ArithmeticFunction ℝ} (hf: ∀ (σ:ℝ), 1 < σ → Summable (fun \end{lemma} %%-/ -lemma first_fourier {ψ:ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompactSupport ψ) {x σ:ℝ} (hx: 0 < x) (hσ: 1 < σ) : ∑' n : ℕ, f n / (n^σ:ℝ) * (fourierIntegral ψ (1 / (2 * π) * log (n / x))) = ∫ t:ℝ, ArithmeticFunction.LSeries f (σ + t * I) * ψ t * x^(t * I) ∂ volume := by +lemma first_fourier {ψ:ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompactSupport ψ) {x σ':ℝ} (hx: 0 < x) (hσ: 1 < σ') : ∑' n : ℕ, f n / (n^σ':ℝ) * (fourierIntegral ψ (1 / (2 * π) * log (n / x))) = ∫ t:ℝ, ArithmeticFunction.LSeries f (σ' + t * I) * ψ t * x^(t * I) ∂ volume := by sorry /-%% @@ -46,7 +46,7 @@ $$ \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du = x^{\si \end{lemma} %%-/ -lemma second_fourier {ψ:ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompactSupport ψ) {x σ:ℝ} (hx: 0 < x) (hσ: 1 < σ) : ∫ u in Set.Ici (-log x), Real.exp (-u * (σ - 1)) * fourierIntegral ψ (u / (2 * π)) = (x^(σ - 1):ℝ) * ∫ t, (1 / (σ + t * I - 1)) * ψ t * x^(t * I) ∂ volume := +lemma second_fourier {ψ:ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompactSupport ψ) {x σ':ℝ} (hx: 0 < x) (hσ: 1 < σ') : ∫ u in Set.Ici (-log x), Real.exp (-u * (σ' - 1)) * fourierIntegral ψ (u / (2 * π)) = (x^(σ' - 1):ℝ) * ∫ t, (1 / (σ' + t * I - 1)) * ψ t * x^(t * I) ∂ volume := sorry /-%% @@ -96,7 +96,7 @@ $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) %%-/ -lemma limiting_fourier {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasCompactSupport ψ) {x:ℝ} (hx: 1 ≤ x) : ∑' n, f(n) / n * fourierIntegral ψ (1/(2*π) * log (n/x)) - A * ∫ u in Set.Ici (-log x), fourierIntegral ψ (u / (2*π)) ∂ volume = ∫ t, (G (1 + I*t)) * (ψ t) * x^(I * t) ∂ volume := by +lemma limiting_fourier {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasCompactSupport ψ) {x:ℝ} (hx: 1 ≤ x) : ∑' n, f n / n * fourierIntegral ψ (1/(2*π) * log (n/x)) - A * ∫ u in Set.Ici (-log x), fourierIntegral ψ (u / (2*π)) ∂ volume = ∫ t, (G (1 + I*t)) * (ψ t) * x^(I * t) ∂ volume := by sorry /-%% @@ -106,20 +106,34 @@ lemma limiting_fourier {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasComp $$ \sum_{n=1}^\infty \frac{f(n)}{n^\sigma} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) - A x^{1-\sigma} \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du = \int_\R G(\sigma+it) \psi(t) x^{it}\ dt.$$ Now take limits as $\sigma \to 1$ using dominated convergence together with \eqref{cheby} and Lemma \ref{decay} to obtain the result. \end{proof} +%%-/ +/-%% \begin{corollary}\label{limiting-cor} With the hypotheses as above, we have $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du + o(1)$$ as $x \to \infty$. \end{corollary} +%%-/ + +open Filter + +lemma limiting_cor {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasCompactSupport ψ) : Tendsto (fun x : ℝ ↦ ∑' n, f n / n * fourierIntegral ψ (1/(2*π) * log (n/x)) - A * ∫ u in Set.Ici (-log x), fourierIntegral ψ (u / (2*π)) ∂ volume) atTop (nhds 0) := by sorry +/-%% \begin{proof} \uses{limiting} Immediate from the Riemann-Lebesgue lemma, and also noting that $\int_{-\infty}^{-\log x} \hat \psi(\frac{u}{2\pi})\ du = o(1)$. \end{proof} +%%-/ +/-%% \begin{lemma}\label{schwarz-id} The previous corollary also holds for functions $\psi$ that are assumed to be in the Schwartz class, as opposed to being $C^2$ and compactly supported. \end{lemma} +%%-/ +lemma limiting_cor_schwartz {ψ: SchwartzMap ℝ ℂ} : Tendsto (fun x : ℝ ↦ ∑' n, f n / n * fourierIntegral ψ (1/(2*π) * log (n/x)) - A * ∫ u in Set.Ici (-log x), fourierIntegral ψ (u / (2*π)) ∂ volume) atTop (nhds 0) := by sorry + +/-%% \begin{proof} \uses{limiting-cor} For any $R>1$, one can use a smooth cutoff function to write $\psi = \psi_{\leq R} + \psi_{>R}$, where $\psi_{\leq R}$ is $C^2$ (in fact smooth) and compactly supported (on $[-R,R]$), and $\psi_{>R}$ obeys bounds of the form @@ -132,19 +146,33 @@ $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi_{>R}( \frac{1}{2\pi} \log \frac{n} $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi_{\leq R}( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi_{\leq R} (\frac{u}{2\pi})\ du + o(1).$$ Combining the two estimates and letting $R$ be large, we obtain the claim. \end{proof} +%%-/ +/-%% \begin{lemma}\label{bij} The Fourier transform is a bijection on the Schwartz class. \end{lemma} +%%-/ +-- just the surjectivity is stated here, as this is all that is needed for the current application, but perhaps one should state and prove bijectivity instead + +lemma fourier_surjection_on_schwartz (f : SchwartzMap ℝ ℂ) : ∃ g : SchwartzMap ℝ ℂ, fourierIntegral g = f := by sorry + +/-%% \begin{proof} This is a standard result in Fourier analysis. \end{proof} +%%-/ +/-%% \begin{corollary}\label{WienerIkeharaSmooth} If $\Psi: (0,\infty) \to \C$ is smooth and compactly supported away from the origin, then, then $$ \sum_{n=1}^\infty f(n) \Psi( \frac{n}{x} ) = A x \int_0^\infty \Psi(y)\ dy + o(x)$$ as $u \to \infty$. \end{corollary} +%%-/ + +lemma wiener_ikehara_smooth {Ψ: ℝ → ℂ} (hsmooth: ∀ n, ContDiff ℝ n Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi (0:ℝ)): Tendsto (fun x : ℝ ↦ (∑' n, f n / n * Ψ (n/x))/x - A * ∫ y in Set.Ioi 0, Ψ y ∂ volume) atTop (nhds 0) := by sorry +/-%% \begin{proof} \uses{bij,schwarz-id} By Lemma \ref{bij}, we can write @@ -153,13 +181,21 @@ for all $y>0$ and some Schwartz function $\psi$. Making this substitution, the $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du + o(1)$$ and the claim follows from Lemma \ref{schwarz-id}. \end{proof} +%%-/ +/-%% \begin{lemma}[Smooth Urysohn lemma]\label{smooth-ury} If $I$ is a closed interval contained in an open interval $J$, then there exists a smooth function $\Psi: \R \to \R$ with $1_I \leq \Psi \leq 1_J$. \end{lemma} +%%-/ +lemma smooth_urysohn {a b c d:ℝ} (h1: a < b) (h2: b