From 6425259e37da6bab0e988f8acefd601de1376ca9 Mon Sep 17 00:00:00 2001
From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com>
Date: Mon, 29 Jan 2024 17:32:32 -0500
Subject: [PATCH] aux lemmata

---
 PrimeNumberTheoremAnd/MellinCalculus.lean | 112 ++++++++++++++++------
 1 file changed, 85 insertions(+), 27 deletions(-)

diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean
index 02991e47..d65ae9dd 100644
--- a/PrimeNumberTheoremAnd/MellinCalculus.lean
+++ b/PrimeNumberTheoremAnd/MellinCalculus.lean
@@ -29,28 +29,42 @@ noncomputable def VerticalIntegral (f : ℂ → ℂ) (σ : ℝ) : ℂ :=
   I • ∫ t : ℝ, f (σ + t * I)
 
 /-%%
-We first prove the following ``Perron-type'' formula.
-\begin{lemma}\label{PerronFormula}
-For $x>0$ and $\sigma>0$, we have
-$$
-\frac1{2\pi i}
-\int_{(\sigma)}\frac{x^s}{s(s+1)}ds = \begin{cases}
-1-\frac1x & \text{ if }x>1\\
-0 & \text{ if } x<1
-\end{cases}.
-$$
-\end{lemma}
+We first prove the following ``Perron-type'' formula, see Lemma \ref{PerronFormula} below.
+This requires some preparatory material.
 %%-/
 
+/-%%
+\begin{lemma}\label{HolomorphicOn_of_Perron_function}\lean{HolomorphicOn_of_Perron_function}
+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{lemma}\label{RectangleIntegral_eq_zero}\lean{RectangleIntegral_eq_zero}
+\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 rectanglet 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}
+\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
@@ -58,21 +72,40 @@ lemma RectangleIntegral_tendsTo_VerticalIntegral {σ σ' : ℝ} (σ_pos : 0 < σ
       (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ)) := by
   sorry
 
+/-%%
+\begin{lemma}\label{PerronIntegralPosAux}\lean{PerronIntegralPosAux}
+The integral
+$$\int_\R\frac{1}{|(1+t)(1+t+1)|}dt$$
+is positive (and hence convergent - since a divergent integral is zero in Lean, by definition).
+\end{lemma}
+%%-/
 lemma PerronIntegralPosAux : 0 < ∫ (t : ℝ), 1 / |(1 + t) * (1 + t + 1)| := by
-
   sorry
 
+/-%%
+\begin{lemma}\label{VertIntPerronBound}\lean{VertIntPerronBound}
+\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)(1+t+1)|}dt.$$
+\end{lemma}
+%%-/
 lemma VertIntPerronBound {x : ℝ} (xpos : 0 < x) (x_le_one : x < 1) {σ : ℝ} (σ_gt_one : 1 < σ) :
-    Complex.abs (VerticalIntegral f σ') ≤ x ^ σ' * ∫ (t : ℝ), 1 / |(1 + t) * (1 + t + 1)| := by
+    Complex.abs (VerticalIntegral f σ) ≤ x ^ σ * ∫ (t : ℝ), 1 / |(1 + t) * (1 + t + 1)| := by
   sorry
 
-
-lemma limitOfConstant {a : ℝ → ℂ} (σ : ℝ) (ha : ∀ᶠ (σ' : ℝ) (σ'' : ℝ) in atTop, a σ' = a σ'')
-    (ha' : Tendsto (fun σ' => a σ') atTop (𝓝 0)) : a σ = 0 := by
+/-%%
+\begin{lemma}\label{limitOfConstant}\lean{limitOfConstant}
+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$.
+%%-/
+lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ) (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (σ'pos : 0 < σ')
+    (σ''pos : 0 < σ''), a σ' = a σ'') (ha' : Tendsto (fun σ' => a σ') atTop (𝓝 0)) : a σ = 0 := by
   sorry
 /-%%
-We break this into the two cases, first proving the following.
-\begin{lemma}\label{PerronFormulaLeOne}\lean{VerticalIntegral_Perron_le_one}
+We are ready for the Perron formula, which breaks into two cases, the first being:
+\begin{lemma}\label{PerronFormulaLtOne}\lean{VerticalIntegral_Perron_lt_one}
 For $x>0$, $\sigma>0$, and $x<1$, we have
 $$
 \frac1{2\pi i}
@@ -80,11 +113,11 @@ $$
 $$
 \end{lemma}
 %%-/
-lemma VerticalIntegral_Perron_le_one {x : ℝ} (xpos : 0 < x) (x_le_one : x < 1)
+lemma VerticalIntegral_Perron_lt_one {x : ℝ} (xpos : 0 < x) (x_lt_one : x < 1)
     {σ : ℝ} (σ_pos : 0 < σ) : VerticalIntegral (fun s ↦ x^s / (s * (s + 1))) σ = 0 := by
 /-%%
 \begin{proof}
-\uses{ResidueTheoremOnRectangle, RectangleIntegralEqSumOfRectangles, VerticalIntegral, MellinTransform}
+\uses{HolomorphicOn_of_Perron_function, RectangleIntegral_eq_zero, PerronIntegralPosAux, VertIntPerronBound, limitOfConstant}
   Let $f(s) = x^s/(s(s+1))$. Then $f$ is holomorphic on the half-plane $\{s\in\mathbb{C}:\Re(s)>0\}$.
 %%-/
   set f : ℂ → ℂ := (fun s ↦ x^s / (s * (s + 1)))
@@ -108,22 +141,47 @@ lemma VerticalIntegral_Perron_le_one {x : ℝ} (xpos : 0 < x) (x_le_one : x < 1)
 --%% $C=\int_\R\frac{1}{|(1+t)(1+t+1)|}dt$.
   have VertIntBound : ∃ C > 0, ∀ σ' > 1, Complex.abs (VerticalIntegral f σ') ≤ x^σ' * C
   · let C := ∫ (t : ℝ), 1 / |(1 + t) * (1 + t + 1)|
-    exact ⟨C, PerronIntegralPosAux, fun σ' σ'_gt_one ↦ VertIntPerronBound xpos x_le_one σ'_gt_one⟩
+    exact ⟨C, PerronIntegralPosAux, fun σ' σ'_gt_one ↦ VertIntPerronBound xpos x_lt_one σ'_gt_one⟩
 --%% Therefore $\int_{(\sigma')}\to 0$ as $\sigma'\to\infty$.
   have VertIntTendsto : Tendsto (fun (σ' : ℝ) ↦ VerticalIntegral f σ') atTop (𝓝 0)
   · have : ‖x‖ < 1 := sorry
     have := tendsto_pow_atTop_nhds_0_of_norm_lt_1 this
     sorry
 --%% So pulling contours gives $\int_{(\sigma)}=0$.
-  refine limitOfConstant (a := fun σ' ↦ VerticalIntegral f σ') σ ?_ VertIntTendsto
-  filter_upwards [mem_atTop 1]
-  intro σ' σ'_ge_one
-  filter_upwards [mem_atTop 1]
-  intro σ'' σ''_ge_one
-  exact contourPull σ' σ'' (by linarith) (by linarith)
+  exact limitOfConstant (a := fun σ' ↦ VerticalIntegral f σ') σ_pos contourPull VertIntTendsto
 --%%\end{proof}
 
 
+/-%%
+The second lemma is the case $x>1$.
+\begin{lemma}\label{PerronFormulaGtOne}\lean{VerticalIntegral_Perron_gt_one}
+For $x>1$ and $\sigma>0$, we have
+$$
+\frac1{2\pi i}
+\int_{(\sigma)}\frac{x^s}{s(s+1)}ds =1-1/x.
+$$
+\end{lemma}
+%%-/
+lemma VerticalIntegral_Perron_gt_one {x : ℝ} (x_gt_one : 1 < x) {σ : ℝ} (σ_pos : 0 < σ) :
+    VerticalIntegral (fun s ↦ x^s / (s * (s + 1))) σ = 1 - 1 / x := by
+  sorry
+
+
+/-%%
+The two together give the Perron formula.
+\begin{lemma}\label{PerronFormula}
+\uses{PerronFormulaLtOne, PerronFormulaGtOne}
+For $x>0$ and $\sigma>0$, we have
+$$
+\frac1{2\pi i}
+\int_{(\sigma)}\frac{x^s}{s(s+1)}ds = \begin{cases}
+1-\frac1x & \text{ if }x>1\\
+0 & \text{ if } x<1
+\end{cases}.
+$$
+\end{lemma}
+%%-/
+
 /-%%
 \begin{theorem}\label{MellinInversion}
 Let $f$ be a nice function from $\mathbb{R}_{>0}$ to $\mathbb{C}$, and let $\sigma$ be sufficiently large. Then