OAI/NumberTheory/TotientAsymptotic/PositiveCoordinateGrid.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous finite-grid rounding of all positive ordered coordinates.

  1. def OAI.TotientAsymptotic.coordinateGridIndex line 11
  2. def OAI.TotientAsymptotic.coordinateGridCutoff line 14
  3. lemma OAI.TotientAsymptotic.positive_coordinate_grid line 17
  4. lemma OAI.TotientAsymptotic.coordinate_grid_cutoff_terminal line 62
  5. lemma OAI.TotientAsymptotic.coordinate_grid_cutoff_descending line 65