OAI/NumberTheory/TotientAsymptotic/PrefixGapVolume.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exponential control of inversions in ordered prime-coordinate regions.

  1. theorem OAI.TotientAsymptotic.prefix_gap_cap_volume line 13
  2. lemma OAI.TotientAsymptotic.prefix_gap_bad_preimage line 66
  3. theorem OAI.TotientAsymptotic.prefix_gap_volume line 81