From 7362f0c2b4b721972179553ae20b08c370c9d2d4 Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Mon, 22 Jan 2024 15:34:34 -0500 Subject: [PATCH] adding `uses` --- .../ResidueCalcOnRectangles.lean | 16 +++- blueprint/Basic.tex | 82 ------------------- blueprint/SecondProofPNT.tex | 8 +- blueprint/blueprint.tex | 16 ++++ 4 files changed, 35 insertions(+), 87 deletions(-) diff --git a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean index ba06260d..c3cd3ce4 100644 --- a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean +++ b/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} diff --git a/blueprint/Basic.tex b/blueprint/Basic.tex index aa4a231d..e69de29b 100644 --- a/blueprint/Basic.tex +++ b/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} - - diff --git a/blueprint/SecondProofPNT.tex b/blueprint/SecondProofPNT.tex index 447026e2..1d1c418b 100644 --- a/blueprint/SecondProofPNT.tex +++ b/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 diff --git a/blueprint/blueprint.tex b/blueprint/blueprint.tex index 3a5e736f..6bbb53a6 100644 --- a/blueprint/blueprint.tex +++ b/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}