OAI/NumberTheory/TotientAsymptotic/CoordinateCubeSize.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The affine unit-box error at one coordinate depends only on its remaining dimension, with the same renewal bound as the total box cost.

  1. lemma OAI.TotientAsymptotic.coordinateCubeShift_sum line 12
  2. lemma OAI.TotientAsymptotic.coordinateCubeShift_le_cost line 43
  3. theorem OAI.TotientAsymptotic.coordinateCubeShift_normalized_bound line 69