OAI/NumberTheory/Ostmann/InverseGoldbach.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ostmann's inverse Goldbach theorem, conditional on the published inputs

  1. theorem OAI.Ostmann.inverseGoldbach_of_published line 13

    Source documentation

    Theorem 1.1: every sum of two nontrivial sets has infinite symmetric difference with the primes. The finite-summand reduction uses Mathlib's Dirichlet theorem; the infinite-summand theorem carries the listed published analytic inputs explicitly.

    theorem inverseGoldbach_of_published
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound) (hBonami : PublishedBonamiBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (CM CH : ℝ) (hM : MertensEstimate CM) (hMH : MertensHarmonicEstimate CH)
    (Z : ∀ χ, ComplexZeroEnumeration χ) (hD : PublishedComplexZeroDensity Z)
    (hR : PublishedComplexZeroRegion Z) (Pexplicit : PublishedSmoothExplicitFormula Z)
    (hPNT : PublishedSmoothPrincipalPNT) : InverseGoldbach := by
…

    Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedBonamiBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.MertensEstimate, OAI.Ostmann.MertensHarmonicEstimate, OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.PublishedSmoothExplicitFormula, OAI.Ostmann.PublishedSmoothPrincipalPNT