OAI/NumberTheory/Ostmann/ZeroDensity/ProgressionConstantRestriction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Decreasing the common exceptional-zero constant

  1. def OAI.Ostmann.PublishedProgressionInput.restrictKappa line 11

    Source documentation

    Completeness and Page uniqueness persist when the exceptional strip is narrowed. The prime-progression estimate and its actual zero are unchanged.

    noncomputable def PublishedProgressionInput.restrictKappa (P : PublishedProgressionInput)
    (κ : ℝ) (hκ : 0 < κ) (hκP : κ ≤ P.kappa) : PublishedProgressionInput where
…

    Mentions: OAI.Ostmann.PublishedProgressionInput