OAI/NumberTheory/TotientAsymptotic/UnbandedGridVolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform volume bound for unbanded enlarged prime-prefix grids.

  1. lemma OAI.TotientAsymptotic.add_pow_le_exp_ratio line 13
  2. theorem OAI.TotientAsymptotic.unbanded_grid_uniform_volume line 25