adding uses

PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean

@@ -44,8 +44,10 @@ noncomputable def RectangleIntegral (f : ℂ → ℂ) (z w : ℂ) : ℂ :=
 abbrev HolomorphicOn (f : ℂ → ℂ) (s : Set ℂ) : Prop := DifferentiableOn ℂ f s
 
 /-%%
-A function is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a
+\begin{definition}\label{MeromorphicOnRectangle}\lean{MeromorphicOnRectangle}\leanok
+A function $f$ is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a
 (finite) set of poles, none of which are on the boundary of the rectangle.
+\end{definition}
 %%-/
 /-- A function is `MeromorphicOnRectangle` if it's holomorphic off of a finite set of `poles`,
   none of which is on the boundary of the rectangle (so the function is continuous there). -/
@@ -64,6 +66,12 @@ is equal to the sum of sufficiently small rectangle integrals around each pole.
     -- ∀ᶠ c in 𝓝[>](0:ℝ),
     -- RectangleIntegral f z w = ∑ p in poles, RectangleIntegral f (p-(c+c*I)) (p+c+c*I) := sorry
 
+/-%%
+\begin{proof}
+\uses{MeromorphicOnRectangle, RectangleIntegral}
+Rectangles tile rectangles, zoom in.
+\end{proof}
+%%-/
 /-%%
 A meromorphic function has a pole of finite order.
 \begin{definition}\label{PoleOrder}
@@ -92,9 +100,9 @@ We can evaluate a small integral around a pole by taking the residue.
 If $f$ has a pole at $z_0$, then every small enough rectangle integral around $z_0$ is equal to $2\pi i Res_{z_0} f$.
 \end{theorem}
 %%-/
-theorem ResidueTheoremOnRectangle (f : ℂ → ℂ) (z₀ : ℂ) (h : MeromorphicAt f z₀) :
-    ∀ᶠ c in 𝓝[>](0:ℝ),
-    RectangleIntegral f (z-(c+c*I)) (z+c+c*I) = 2*π*I* Res f z₀ := sorry
+-- theorem ResidueTheoremOnRectangle (f : ℂ → ℂ) (z₀ : ℂ) (h : MeromorphicAt f z₀) :
+--     ∀ᶠ c in 𝓝[>](0:ℝ),
+--     RectangleIntegral f (z-(c+c*I)) (z+c+c*I) = 2*π*I* Res f z₀ := sorry
 
 /-%%
 \begin{proof}

blueprint/Basic.tex

@@ -1,82 +0,0 @@
-
-
-In this file, we prove the Prime Number Theorem. Continuations of this project aim to extend
-this work to primes in progressions (Dirichlet's theorem), Chebytarev's density theorem, etc
-etc.
-
-
-
-
-A function is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a
-(finite) set of poles, none of which are on the boundary of the rectangle.
-
-
-
-Discuss polar behavior of meromorphic functions
-
-A
-
-
-
-
-We show that if a function is meromorphic on a rectangle, then the rectangle integral of the
-function is equal to the sum of the residues of the function at its poles.
-
-
-
-MellinTransform
-
-Mellin Inversion (Goldfeld-Kontorovich)
-
-ChebyshevPsi
-
-ZeroFreeRegion
-
-Hadamard Factorization
-
-Hoffstein-Lockhart + Goldfeld-Hoffstein-Liemann
-
-LSeries (NatPos->C)
-
-RiemannZetaFunction
-
-RectangleIntegral
-
-ResidueTheoremOnRectangle
-
-ArgumentPrincipleOnRectangle
-
-Break rectangle into lots of little rectangles where f is holomorphic, and squares with center at a pole
-
-HasPoleAt f z : TendsTo 1/f (N 0)
-
-Equiv: TendsTo f atTop
-
-Then locally f looks like (z-z_0)^N g
-
-For all c sufficiently small, integral over big rectangle with finitely many poles is equal to rectangle integral localized at each pole.
-Rectangles tile rectangles! (But not circles -> circles) No need for toy contours!
-
-
-
-
-\begin{definition}
-The Chebyshev Psi function is defined as
-$$
-\psi(x) = \sum_{n \leq x} \Lambda(n),
-$$
-where $\Lambda(n)$ is the von Mangoldt function.
-\end{definition}
-
-
-
-
-Main Theorem: The Prime Number Theorem
-\begin{theorem}[PrimeNumberTheorem]
-$$
-ψ (x) = x + O(x e^{-c \sqrt{\log x}})
-$$
-as $x\to \infty$.
-\end{theorem}
-
-

blueprint/SecondProofPNT.tex

@@ -73,7 +73,13 @@
 
 
 Then, since $\zeta$ doesn't vanish on the 1-line, there is a $\delta$ (depending on $T$), so that the box $[1-\delta,1] \times_{ℂ} [-T,T]$ is free of zeros of $\zeta$.
+The rectangle with opposite corners $1-\delta - i T$ and $2+iT$ contains a single pole of $-\zeta'/\zeta$ at $s=1$, and the residue is $1$ (from Theorem \ref{ResidueOfLogDerivative}).
+\begin{theorem}\label{ZeroFreeBox}
+$-\zeta'/\zeta$ is holomorphic on the box $[1-\delta,2] \times_{ℂ} [-T,T]$, except a simple pole with residue $1$ at $s$=1.
+\end{theorem}
+
+
 
-The rectangle integral with opposite corners $1-\delta - i T$ and $2+iT$ contains a single pole of $-\zeta'/\zeta$ at $s=1$, and the residue is $1$ (from Theorem \ref{ResidueOfLogDerivative}).
+Inserting this into $\psi_{\epsilon}$, we get
 
 

blueprint/blueprint.tex

@@ -66,4 +66,20 @@ \section{Hoffstein-Lockhart}
 \section{Strong PNT}
 \input{StrongPNT.tex}
 
+\chapter{Elementary Corollaries}
+
+Some things to work on next:
+
+Prime counting function is asymptotic to the logarithmic integral
+
+Asymptotics for Moebius sum
+
+The $n$prime prime is asymptotic to $p_n \sim n \log n$
+
+Summing log's only over primes (not prime powers; Chebychev's ``first'' function)
+
+The $n$th primordial (product of first $n$ primes) is $=e^{(1+o(1))n\log n}$
+
+
+
 \end{document}