OAI/NumberTheory/Ostmann/Construction/PrimeLogGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete equal-mesh log cells and unit residues

  1. def OAI.Ostmann.gridLower line 12
  2. def OAI.Ostmann.gridUpper line 15
  3. def OAI.Ostmann.gridResidue line 18
  4. theorem OAI.Ostmann.grid_separated line 21
  5. def OAI.Ostmann.gridPrimeCellPartition line 46

    Source documentation

    The finite cells used for idealization are constructed directly from an equal-mesh logarithmic grid and every invertible residue class.

    noncomputable def gridPrimeCellPartition (N q : ℕ) [NeZero q]
    (hN : 0 < N) (s h : ℝ) (hs : 1 ≤ s) (hh : 0 ≤ h) (hh1 : h ≤ 1) :
    PrimeCellPartition
      (primeCellSupport q (gridResidue (N := N) (q := q)) (gridLower s h) (gridUpper s h))
…

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

  6. theorem OAI.Ostmann.mem_primeLogCellSet_iff line 62