diff --git a/PrimeNumberTheoremAnd/AuxiliaryLemmata.lean b/PrimeNumberTheoremAnd/AuxiliaryLemmata.lean deleted file mode 100644 index 78048a0f..00000000 --- a/PrimeNumberTheoremAnd/AuxiliaryLemmata.lean +++ /dev/null @@ -1,139 +0,0 @@ -import Mathlib.Analysis.Complex.CauchyIntegral - -open Complex Topology Filter - -open scoped Interval - - -/-%% -\begin{definition}\label{Rectangle}\lean{Rectangle}\leanok -A Rectangle has corners $z$ and $w \in \C$. -\end{definition} -%%-/ -/-- A `Rectangle` has corners `z` and `w`. -/ -def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]] - -/-%% -\begin{definition}\label{RectangleIntegral}\lean{RectangleIntegral}\leanok -A RectangleIntegral of a function $f$ is one over a rectangle determined by $z$ and $w$ in $\C$. -\end{definition} -%%-/ -/-- A `RectangleIntegral` of a function `f` is one over a rectangle determined by - `z` and `w` in `ℂ`. -/ -noncomputable def RectangleIntegral (f : ℂ → ℂ) (z w : ℂ) : ℂ := - (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) - + I • (∫ y : ℝ in z.im..w.im, f (w.re + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (z.re + y * I) - -/-- A function is `HolomorphicOn` a set if it is complex differentiable on that set. -/ -abbrev HolomorphicOn (f : ℂ → ℂ) (s : Set ℂ) : Prop := DifferentiableOn ℂ f s - -/-%% -It is very convenient to define integrals along vertical lines in the complex plane, as follows. -\begin{definition}\label{VerticalIntegral}\leanok -Let $f$ be a function from $\mathbb{C}$ to $\mathbb{C}$, and let $\sigma$ be a real number. Then we define -$$\int_{(\sigma)}f(s)ds = \int_{\sigma-i\infty}^{\sigma+i\infty}f(s)ds.$$ -\end{definition} -[Note: Better to define $\int_{(\sigma)}$ as $\frac1{2\pi i}\int_{\sigma-i\infty}^{\sigma+i\infty}$?? -There's a factor of $2\pi i$ in such contour integrals...] -%%-/ - -noncomputable def VerticalIntegral (f : ℂ → ℂ) (σ : ℝ) : ℂ := - I • ∫ t : ℝ, f (σ + t * I) - -/-%% -The following is preparatory material used in the proof of the Perron formula, see Lemma \ref{PerronFormula}. -%%-/ - -/-%% -\begin{lemma}\label{HolomorphicOn_of_Perron_function}\lean{HolomorphicOn_of_Perron_function}\leanok -Let $x>0$. Then the function $f(s) = x^s/(s(s+1))$ is holomorphic on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$. -\end{lemma} -%%-/ -lemma HolomorphicOn_of_Perron_function {x : ℝ} (xpos : 0 < x) : - HolomorphicOn (fun s => x ^ s / (s * (s + 1))) {s | 0 < s.re} := by - sorry -/-%% -\begin{proof} -Chain differentiabilities. -\end{proof} -%%-/ - -/-%% -\begin{lemma}\label{RectangleIntegral_eq_zero}\lean{RectangleIntegral_eq_zero}\leanok -\uses{RectangleIntegral} -Let $\sigma,\sigma',T>0$, and let $f$ be a holomorphic function on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$. Then -the rectangle integral -$$\int_{\sigma-iT}^{\sigma'+iT}f(s)ds = 0.$$ -\end{lemma} -%%-/ - -lemma RectangleIntegral_eq_zero {σ σ' T : ℝ} (σ_pos : 0 < σ) (σ'_pos : 0 < σ') (T_pos : 0 < T) - {f : ℂ → ℂ} (fHolo : HolomorphicOn f {s | 0 < s.re}) : - RectangleIntegral f (σ - I * T) (σ' + I * T) = 0 := by - sorry -- apply HolomorphicOn.vanishesOnRectangle in PR #9598 - -/-%% -\begin{lemma}\label{RectangleIntegral_tendsTo_VerticalIntegral}\lean{RectangleIntegral_tendsTo_VerticalIntegral}\leanok -\uses{RectangleIntegral} -Let $\sigma,\sigma'>0$, and let $f$ be a holomorphic function on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$. Then -the limit of rectangle integrals -$$\lim_{T\to\infty}\int_{\sigma-iT}^{\sigma'+iT}f(s)ds = \int_{(\sigma')}f(s)ds - \int_{(\sigma)}f(s)ds -.$$ -*** Needs more conditions on $f$ *** -\end{lemma} -%%-/ - -lemma RectangleIntegral_tendsTo_VerticalIntegral {σ σ' : ℝ} (σ_pos : 0 < σ) (σ'_pos : 0 < σ') - {f : ℂ → ℂ} (fHolo : HolomorphicOn f {s | 0 < s.re}) : - -- needs more hypotheses - Tendsto (fun (T : ℝ) ↦ RectangleIntegral f (σ - I * T) (σ' + I * T)) atTop - (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ)) := by - sorry - -/-%% -\begin{lemma}\label{PerronIntegralPosAux}\lean{PerronIntegralPosAux}\leanok -The integral -$$\int_\R\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt$$ -is positive (and hence convergent - since a divergent integral is zero in Lean, by definition). -\end{lemma} -%%-/ -lemma PerronIntegralPosAux : 0 < ∫ (t : ℝ), 1 / |Real.sqrt (1 + t^2) * Real.sqrt (2 + t^2)| := by - sorry -/-%% -\begin{proof} -Standard estimate. -\end{proof} -%%-/ - -/-%% -\begin{lemma}\label{VertIntPerronBound}\lean{VertIntPerronBound}\leanok -\uses{VerticalIntegral} -Let $x>0$, $\sigma>1$, and $x<1$. Then -$$\left| -\int_{(\sigma)}\frac{x^s}{s(s+1)}ds\right| \leq x^\sigma \int_\R\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt.$$ -\end{lemma} -%%-/ - -lemma VertIntPerronBound {x : ℝ} (xpos : 0 < x) (x_le_one : x < 1) {σ : ℝ} (σ_gt_one : 1 < σ) : - Complex.abs (VerticalIntegral (fun s ↦ x^s / (s * (s + 1))) σ) - ≤ x ^ σ * ∫ (t : ℝ), 1 / |Real.sqrt (1 + t^2) * Real.sqrt (2 + t^2)| := by - sorry - -/-%% -\begin{lemma}\label{limitOfConstant}\lean{limitOfConstant}\leanok -Let $a:\R\to\C$ be a function, and let $\sigma>0$ be a real number. Suppose that, for all -$\sigma, \sigma'>0$, we have $a(\sigma')=a(\sigma)$, and that -$\lim_{\sigma\to\infty}a(\sigma)=0$. Then $a(\sigma)=0$. -\end{lemma} -%%-/ -lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ) (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (σ'pos : 0 < σ') - (σ''pos : 0 < σ''), a σ' = a σ'') (ha' : Tendsto (fun σ' => a σ') atTop (𝓝 0)) : a σ = 0 := by - sorry -/-%% -\begin{proof} -To show that $a(\sigma)=0$, we show that $a(\sigma)< \epsilon$ for all $\epsilon>0$. Let $\epsilon>0$. -The fact that $\lim_{\sigma\to\infty}a(\sigma)=0$ means that there exists $\sigma_0>0$ such that -$|a(\sigma)|<\epsilon$ for all $\sigma>\sigma_0$. Now let $\sigma>0$. Then $a(\sigma)=a(\sigma_0)$, and -so $|a(\sigma)|=|a(\sigma_0)|<\epsilon$, as required. -\end{proof} -%%-/ diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean index 7d82266f..67b0988e 100644 --- a/PrimeNumberTheoremAnd/MellinCalculus.lean +++ b/PrimeNumberTheoremAnd/MellinCalculus.lean @@ -8,21 +8,35 @@ open Complex Topology Filter In this section, we define the Mellin transform (already in Mathlib, thanks to David Loeffler), prove its inversion formula, and derive a number of important properties of some special functions and bumpfunctions. -\begin{definition}\label{MellinTransform} +Def: (Already in Mathlib) Let $f$ be a function from $\mathbb{R}_{>0}$ to $\mathbb{C}$. We define the Mellin transform of $f$ to be the function $\mathcal{M}(f)$ from $\mathbb{C}$ to $\mathbb{C}$ defined by $$\mathcal{M}(f)(s) = \int_0^\infty f(x)x^{s-1}dx.$$ -\end{definition} [Note: My preferred way to think about this is that we are integrating over the multiplicative group $\mathbb{R}_{>0}$, multiplying by a (not necessarily unitary!) character $|\cdot|^s$, and integrating with respect to the invariant Haar measure $dx/x$. This is very useful in the kinds of calculations carried out below. But may be more difficult to formalize as things now stand. So we might have clunkier calculations, which ``magically'' turn out just right - of course they're explained by the aforementioned structure...] %%-/ + /-%% -We need some auxiliary lemmata. +It is very convenient to define integrals along vertical lines in the complex plane, as follows. +\begin{definition}\label{VerticalIntegral}\leanok +Let $f$ be a function from $\mathbb{C}$ to $\mathbb{C}$, and let $\sigma$ be a real number. Then we define +$$\int_{(\sigma)}f(s)ds = \int_{\sigma-i\infty}^{\sigma+i\infty}f(s)ds.$$ +\end{definition} +[Note: Better to define $\int_{(\sigma)}$ as $\frac1{2\pi i}\int_{\sigma-i\infty}^{\sigma+i\infty}$?? +There's a factor of $2\pi i$ in such contour integrals...] +%%-/ + +noncomputable def VerticalIntegral (f : ℂ → ℂ) (σ : ℝ) : ℂ := + I • ∫ t : ℝ, f (σ + t * I) -%** Note : move aux stuff back into here! ** +/-%% +The following is preparatory material used in the proof of the Perron formula, see Lemma \ref{PerronFormula}. +%%-/ + +/-%% \begin{lemma}\label{zeroTendstoDiff}\lean{zeroTendstoDiff}\leanok If the limit of $0$ is $L₁ - L₂$, then $L₁ = L₂$. \end{lemma} @@ -37,9 +51,121 @@ Obvious. %%-/ +/-%% +\begin{lemma}\label{HolomorphicOn_of_Perron_function}\lean{HolomorphicOn_of_Perron_function}\leanok +Let $x>0$. Then the function $f(s) = x^s/(s(s+1))$ is holomorphic on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$. +\end{lemma} +%%-/ +lemma HolomorphicOn_of_Perron_function {x : ℝ} (xpos : 0 < x) : + HolomorphicOn (fun s => x ^ s / (s * (s + 1))) {s | 0 < s.re} := by + sorry +/-%% +\begin{proof} +Composition of differentiabilities. +\end{proof} +%%-/ + +/-%% +\begin{lemma}\label{RectangleIntegral_eq_zero}\lean{RectangleIntegral_eq_zero}\leanok +\uses{RectangleIntegral} +Let $\sigma,\sigma',T>0$, and let $f$ be a holomorphic function on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$. Then +the rectangle integral +$$\int_{\sigma-iT}^{\sigma'+iT}f(s)ds = 0.$$ +\end{lemma} +%%-/ +lemma RectangleIntegral_eq_zero {σ σ' T : ℝ} (σ_pos : 0 < σ) (σ'_pos : 0 < σ') (T_pos : 0 < T) + {f : ℂ → ℂ} (fHolo : HolomorphicOn f {s | 0 < s.re}) : + RectangleIntegral f (σ - I * T) (σ' + I * T) = 0 := by + sorry -- apply HolomorphicOn.vanishesOnRectangle in PR #9598 +/-%% +\begin{proof} +This almost exists in a Mathlib PR, needs to be adapted here. +(HolomorphicOn.vanishesOnRectangle in PR \#9598) +\end{proof} +%%-/ + + +/-%% +\begin{lemma}\label{RectangleIntegral_tendsTo_VerticalIntegral}\lean{RectangleIntegral_tendsTo_VerticalIntegral}\leanok +\uses{RectangleIntegral} +Let $\sigma,\sigma'>0$, and let $f$ be a holomorphic function on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$. Then +the limit of rectangle integrals +$$\lim_{T\to\infty}\int_{\sigma-iT}^{\sigma'+iT}f(s)ds = \int_{(\sigma')}f(s)ds - \int_{(\sigma)}f(s)ds +.$$ +*** Needs more conditions on $f$ *** +\end{lemma} +%%-/ + +lemma RectangleIntegral_tendsTo_VerticalIntegral {σ σ' : ℝ} (σ_pos : 0 < σ) (σ'_pos : 0 < σ') + {f : ℂ → ℂ} (fHolo : HolomorphicOn f {s | 0 < s.re}) : + -- needs more hypotheses + Tendsto (fun (T : ℝ) ↦ RectangleIntegral f (σ - I * T) (σ' + I * T)) atTop + (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ)) := by + sorry +/-%% +\begin{proof} +Almost by definition. +\end{proof} +%%-/ + + +/-%% +\begin{lemma}\label{PerronIntegralPosAux}\lean{PerronIntegralPosAux}\leanok +The integral +$$\int_\R\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt$$ +is positive (and hence convergent - since a divergent integral is zero in Lean, by definition). +\end{lemma} +%%-/ +lemma PerronIntegralPosAux : 0 < ∫ (t : ℝ), 1 / |Real.sqrt (1 + t^2) * Real.sqrt (2 + t^2)| := by + sorry +/-%% +\begin{proof} +Standard estimate. +\end{proof} +%%-/ + +/-%% +\begin{lemma}\label{VertIntPerronBound}\lean{VertIntPerronBound}\leanok +\uses{VerticalIntegral} +Let $x>0$, $\sigma>1$, and $x<1$. Then +$$\left| +\int_{(\sigma)}\frac{x^s}{s(s+1)}ds\right| \leq x^\sigma \int_\R\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt.$$ +\end{lemma} +%%-/ + +lemma VertIntPerronBound {x : ℝ} (xpos : 0 < x) (x_le_one : x < 1) {σ : ℝ} (σ_gt_one : 1 < σ) : + Complex.abs (VerticalIntegral (fun s ↦ x^s / (s * (s + 1))) σ) + ≤ x ^ σ * ∫ (t : ℝ), 1 / |Real.sqrt (1 + t^2) * Real.sqrt (2 + t^2)| := by + sorry +/-%% +\begin{proof} +Triangle inequality and pointwise estimate. +\end{proof} +%%-/ + +/-%% +\begin{lemma}\label{limitOfConstant}\lean{limitOfConstant}\leanok +Let $a:\R\to\C$ be a function, and let $\sigma>0$ be a real number. Suppose that, for all +$\sigma, \sigma'>0$, we have $a(\sigma')=a(\sigma)$, and that +$\lim_{\sigma\to\infty}a(\sigma)=0$. Then $a(\sigma)=0$. +\end{lemma} +%%-/ +lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ) (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (σ'pos : 0 < σ') + (σ''pos : 0 < σ''), a σ' = a σ'') (ha' : Tendsto (fun σ' => a σ') atTop (𝓝 0)) : a σ = 0 := by + sorry +/-%% +\begin{proof} +To show that $a(\sigma)=0$, we show that $a(\sigma)< \epsilon$ for all $\epsilon>0$. Let $\epsilon>0$. +The fact that $\lim_{\sigma\to\infty}a(\sigma)=0$ means that there exists $\sigma_0>0$ such that +$|a(\sigma)|<\epsilon$ for all $\sigma>\sigma_0$. Now let $\sigma>0$. Then $a(\sigma)=a(\sigma_0)$, and +so $|a(\sigma)|=|a(\sigma_0)|<\epsilon$, as required. +\end{proof} +%%-/ + + /-%% We are ready for the Perron formula, which breaks into two cases, the first being: -\begin{lemma}\label{PerronFormulaLtOne}\lean{VerticalIntegral_Perron_lt_one} +\begin{lemma}\label{PerronFormulaLtOne}\lean{VerticalIntegral_Perron_lt_one}\leanok For $x>0$, $\sigma>0$, and $x<1$, we have $$ \frac1{2\pi i} diff --git a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean index b0e65477..0bd11a68 100644 --- a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean +++ b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean @@ -4,7 +4,7 @@ import Mathlib.NumberTheory.ArithmeticFunction import Mathlib.NumberTheory.ZetaFunction import Mathlib.Analysis.Analytic.Meromorphic import PrimeNumberTheoremAnd.EulerProducts.LSeries -import PrimeNumberTheoremAnd.AuxiliaryLemmata + open Complex BigOperators Finset Nat Classical @@ -14,6 +14,28 @@ open scoped ArithmeticFunction Interval In this file, we develop residue calculus on rectangles. +\begin{definition}\label{Rectangle}\lean{Rectangle}\leanok +A Rectangle has corners $z$ and $w \in \C$. +\end{definition} +%%-/ +/-- A `Rectangle` has corners `z` and `w`. -/ +def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]] + +/-%% +\begin{definition}\label{RectangleIntegral}\lean{RectangleIntegral}\leanok +A RectangleIntegral of a function $f$ is one over a rectangle determined by $z$ and $w$ in $\C$. +\end{definition} +%%-/ +/-- A `RectangleIntegral` of a function `f` is one over a rectangle determined by + `z` and `w` in `ℂ`. -/ +noncomputable def RectangleIntegral (f : ℂ → ℂ) (z w : ℂ) : ℂ := + (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) + + I • (∫ y : ℝ in z.im..w.im, f (w.re + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (z.re + y * I) + +/-- A function is `HolomorphicOn` a set if it is complex differentiable on that set. -/ +abbrev HolomorphicOn (f : ℂ → ℂ) (s : Set ℂ) : Prop := DifferentiableOn ℂ f s + +/-%% The border of a rectangle is the union of its four sides. \begin{definition}\label{RectangleBorder}\lean{RectangleBorder}\leanok A Rectangle's border, given corners $z$ and $w$ is the union of the four sides. @@ -66,6 +88,7 @@ $$ [Note: There is a recent PR by David Loeffler dealing with orders of poles.] %%-/ + /-%% If a meromorphic function $f$ has a pole at $z_0$, then the residue of $f$ at $z_0$ is the coefficient of $1/(z-z_0)$ in the Laurent series of $f$ around $z_0$. \begin{definition}\label{Residue}