OAI/NumberTheory/Ostmann/Construction/PrimeGridSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The grid covers exactly the original prime interval

  1. theorem OAI.Ostmann.mem_gridPrimeSupport_iff line 11
  2. theorem OAI.Ostmann.mem_gridPrimeSupport_iff_prime line 44

    Source documentation

    At these scales the modulus is below every sampled prime, so every prime in the log interval appears in the unit-residue grid.

    theorem mem_gridPrimeSupport_iff_prime (N q : ℕ) [NeZero q] (s h : ℝ)
    (hh : 0 ≤ h) (hq : (q : ℝ) ≤ Real.exp s) (p : ℕ) :
    p ∈ primeCellSupport q (gridResidue (N := N) (q := q)) (gridLower s h) (gridUpper s h) ↔
…

    Mentions: OAI.Ostmann.primeCellSupport, OAI.Ostmann.gridResidue, OAI.Ostmann.gridLower, OAI.Ostmann.gridUpper