dependency work

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}

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}