Repository for formalizations related to RH/zeta

Stream: maths

[Matteo Cipollina]

Late in October, Jonathan Washburn asked me to review and help him improve his Lean formalization on work related to zeta function.

We believe that it may be beneficial to begin to start to share with this community some of the lean work done together, for comments and for collaboration (we left some sorries to fill in a few files ).

https://github.com/jonwashburn/riemann
https://github.com/jonwashburn/riemann/blob/main/Riemann.lean

The repository includes substantial infrastructure (and prerequisites) for:

• DeBranges space,
• Hardy space, PoissonKernel
• Nevanlinna theory,
• Carleson measure, BMO and many others (mainly under Riemann/Mathlib);
• substantial development of the GibbsMeasure API (from @YaelDillies repository),
• a formalization of mean field theory and spin glass (following Talagrand chapt 1, 2 - under Riemann/PhysLean/SpinGlass - and leveraging my previous formalization of Gaussian Integration by parts) and its application to arithmetic and zeta;
• partial formalization of some research papers (by Connes, Kapustin, Arguin, Arguin-Radziwill and by the authors in Notes/Papers/CW).

Among the main theorems that can be found are:

• Hadamard factorization (from PrimeNumberTheoremAnd ),
• Cartan’s formula (from VD),
• Binet integral, Binet formula and other bounds related to Gamma,
• Robbins and Stirling bounds (in Riemann.Mathlib/Analysis.SpecialFunctions.StirlingRobbins),
• Theorems on the existence of GibbsMeasure, Guerra interpolation (in several formulations, including arithmetic, though not yet in the full setting of Talagrand vol 2 - for which GibbsMeasure development was needed, as well as the mathlib PR on CameronMartin),
• JohnNiremberg inequality, and many others

To ensure integration with the larger ecosystem and future mathlib we have made effort to port and integrate, actively and in perspective, some of the main external repositories not yet in mathlib that were relevant for RH. While the integration will progress, this has allowed us to leverage PrimeNumberTheoremAnd and StrongPNT, Carleson, VD, GibbsMeasure, DeRhamCohomolgy. We have also added PhysLean as it allow us to leverage the API in the QuantumMechanics folder to formalize idiomatically other papers that are prerequisities for those Jonathan is working on.

[The work is funded as part of the research of Recognition Physics Research Institute, which is being funded by Jonathan.]

[Yaël Dillies]

Would you be happy to contribute back to GibbsMeasure? :slight_smile:

[Matteo Cipollina]

Of course, that API naturally belongs there and I would find very impolite not to contribute it back. Will do soon and will be very grateful if you could find time to review it at some point :) Thanks!

[Yaël Dillies]

Gladly!

[Ruben Van de Velde]

Are you also submitting results to mathlib?

[Matteo Cipollina]

Yes, time permitting that is also the goal. We have tried to keep many things (definitely not all) organized in Mathlib folders to facilitate identifying what would be fit, and we have really made effort to design things in their own right rather than from the specific angle we needed.
Possibly a good start would be Cartan, and I have already PRd Cartan.lean to VD folder (@Stefan Kebekus - thanks! ) but, like everything in the repo, it requires a big clean-up and golfing before being ready for a mathlib review (and possibly extracting some general lemmas and provide more core API).

[Yongxi Lin (Aaron)]

I would love to contribute to the part about Hardy spaces and BMO, but I didn't find the file CONTRIBUTING.md :smiling_face_with_tear:

[Matteo Cipollina]

Yongxi Lin (Aaron) ha scritto:

I would love to contribute to the part about Hardy spaces and BMO, but I didn't find the file CONTRIBUTING.md :smiling_face_with_tear:

Hi, thank you for your message! It would be great if you could contribute to the repository. I think Fatou's theorem would be a good target, or the CanonicalFactorization file, please feel free to open a PR or DM me for any help.

[Matteo Cipollina]

Update: The formalization of the Hadamard Factorization theorem for entire functions of finite order has been upgraded to establish a sharp degree bound for the exponential factor ($p \le \lfloor \rho \rfloor$). To achieve this, we formalized the minimum modulus principle using the 'probabilistic radius' argument (following Tao’s notes). In this way the result should be in line with the expected formulation for the PNT+ repository.

https://github.com/jonwashburn/riemann/blob/main/Riemann/academic_framework/HadamardFactorization/Main.lean

This PR applies it to zeta function as a corollary.

We aim to contribute this to Mathlib, though the current implementation relies on a custom ZeroData structure which has proved effective in formalizing the proof, but that somewhat isolates it from the library's standard API. We introduced ZeroData as a way to integrate mathlib's Divisor (which models zeros algebraically/geometrically) and the tprod API (which requires an indexed sequence). ZeroData bundles the enumeration of zeros with their local finiteness properties, so one can decouple the analytic proofs from combinatorially converting a divisor support into a sequence, and use a 'padding' hack to handle finite vs infinite sums uniformly.

Time permitting, we have started working on refactoring the code to contribute it to mathlib focusing on the below tasks, any suggestions or collaboration throughout the process is welcome :

1. Reformulate the main theorem to accept an f : ℂ → ℂ and a D : Divisor ℂ directly.
2. Derive the sequence a_n from the divisor support (or define the canonical product directly over the divisor).
3. Systematically leverage the Filter and Asymptotics APIs to replace remaining manual epsilon-delta steps .

structure ZeroData (f : ℂ → ℂ) where
  /-- A sequence enumerating the nonzero zeros. Values of `0` are ignored/padding. -/
  zeros : ℕ → ℂ
  /-- Local finiteness: only finitely many *nonzero* zeros land in any closed ball. -/
  finite_in_ball : ∀ R : ℝ, ({n : ℕ | zeros n ≠ 0 ∧ ‖zeros n‖ ≤ R} : Set ℕ).Finite
  /-- Order of vanishing at `0`. -/
  ord0 : ℕ
  /-- `ord0` is the actual vanishing order of `f` at `0`. -/
  ord0_spec : analyticOrderNatAt f 0 = ord0
  /-- Multiplicity specification: the analytic order at each nonzero zero is the count in the sequence. -/
  zeros_mult_spec :
    ∀ z : ℂ, z ≠ 0 → analyticOrderNatAt f z = Nat.card {n : ℕ // zeros n = z}
  /-- Specification of the zero set of `f`. -/
  zero_spec : ∀ z : ℂ, f z = 0 ↔
    (z = 0 ∧ 0 < ord0) ∨ (z ≠ 0 ∧ ∃ n, zeros n = z)

theorem hadamard_factorization
    {ρ : ℝ} {f : ℂ → ℂ}
    (hρ : 0 ≤ ρ)
    (hf : EntireOfFiniteOrder ρ f)
    (hz : ZeroData f) :
    ∃ (P : Polynomial ℂ),
      P.degree ≤ (Nat.floor ρ) ∧
      ∀ z : ℂ,
        f z = Complex.exp (Polynomial.eval z P) *
          z ^ hz.ord0 *
          ∏' n : ℕ, (ComplexAnalysis.Hadamard.weierstrassFactor (Nat.floor ρ) (z / hz.zeros n)) := by sorry -- proof in the repository