OAI/NumberTheory/Ostmann/QuadraticCenter/ClosedQuadraticBand.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.closedLogPrimeBand line 13
2. def OAI.Ostmann.closedQuadraticBandMass line 16
3. theorem OAI.Ostmann.mem_closedLogPrimeBand_iff line 19
4. theorem OAI.Ostmann.logPrimeBand_subset_closed line 29
5. theorem OAI.Ostmann.deleted_log_eq line 34
6. theorem OAI.Ostmann.closedQuadraticBandMass_le line 46
7. theorem OAI.Ostmann.closedQuadraticBandMass_nonneg line 75
8. theorem OAI.Ostmann.closedQuadraticBandMass_isLittleO_of_halfopen line 83
9. theorem OAI.Ostmann.EventuallyPrimeSumset.quadratic_smallness line 97

   Source documentation

   Proposition 3.1 with its exact closed prime band, conditionally only on the recorded published inputs. The positive Fourier cutoff is constructed.

   theorem EventuallyPrimeSumset.quadratic_smallness
       {A B : Set ℕ} (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite)
       (hBonami : PublishedBonamiBound) (P₀ : PublishedProgressionInput)
       (H : PublishedRealZeroInput P₀) (hSiegel : PublishedSiegelBound)
       (sieve : PublishedQuadraticLargeSieve) (hsize : PublishedSummandSizeBound)
       (C₀ : ℝ) (hM : MertensEstimate C₀) :
       ∃ N, (∀ p, p.Prime → Disjoint (tailResidues A N p) (negTailResidues B N p)) ∧
         (fun T => closedQuadraticBandMass A N T) =o[atTop] (fun T : ℝ => T) := by
   …

   Mentions: OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.PublishedBonamiBound, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.MertensEstimate, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.closedQuadraticBandMass