updating mathlib

.lake/lakefile.olean.trace

@@ -1,4 +1,4 @@
 {"platform": "macOS-64",
  "options": {},
  "leanHash": "b614ff1d12bc38f39077f9ce9f2d48b42c003ad0",
- "configHash": "14702514882803425136"}
+ "configHash": "6829288224078697752"}

PrimeNumberTheoremAnd/Basic.lean

@@ -2,14 +2,56 @@ import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.NumberTheory.VonMangoldt
 import Mathlib.NumberTheory.ArithmeticFunction
 import Mathlib.NumberTheory.ZetaFunction
+import Mathlib.Analysis.Analytic.Meromorphic
 
 open Complex BigOperators Finset Nat Classical
 
-open scoped ArithmeticFunction
+open scoped ArithmeticFunction Interval
 
 /-%%
 
-In this file, we prove the Prime Number Theorem. We have plans to extend to primes in progressions (Dirichlet's theorem), Chebytarev's density theorem, etc etc.
+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 `Rectangle` has corners `z` and `w`. -/
+def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]]
+
+/-- A `RectangleBorder` has corners `z` and `w`. -/
+def RectangleBorder (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ {z.im} ∪ {z.re} ×ℂ [[z.im, w.im]] ∪ [[z.re, w.re]] ×ℂ {w.im} ∪ {w.re} ×ℂ [[z.im, w.im]]
+
+/-- A function is `HolomorphicOn` a set if it is complex differentiable on that set. -/
+abbrev HolomorphicOn (f : ℂ → ℂ) (s : Set ℂ) : Prop := DifferentiableOn ℂ f s
+
+/-- A function is `MeromorphicOnRectangle`  -/
+class MeromorphicOnRectangle (f : ℂ → ℂ) (poles : Set ℂ) (z w : ℂ) : Prop where
+  holomorphicOn : HolomorphicOn f ((Rectangle z w) ∩ polesᶜ)
+  hasPoleAt : ∀ p ∈ poles, MeromorphicAt f p
+  continuousOn : ContinuousOn f (RectangleBorder z w)
+/-%%
+Class MeromorphicOnRectangle (f)
+Theorem ResidueOnRectangle
+MellinTransform
+Mellin Inversion (Goldfeld-Kontorovich)
+ChebyshevPsi
+ZeroFreeRegion
+Hadamard Factorization
+Hoffstein-Lockhart + Goldfeld-Hoffstein-Liemann
+9-12 and 2-5 every day
+DirichletSeries (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{def}
 The Chebyshev Psi function is defined as

lakefile.lean

@@ -8,7 +8,7 @@ lean_lib «PrimeNumberTheoremAnd» where
   -- add library configuration options here
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"25bcbbb"
+  "https://github.com/leanprover-community/mathlib4.git"@"e659b1b"
 
 meta if get_config? env = some "dev" then require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "29f7f43"