OAI/NumberTheory/TotientAsymptotic/OrderedTranslateVolume.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive volume of the ordered part of a renewal translate.

  1. def OAI.TotientAsymptotic.orderedSlackRegion line 12
  2. lemma OAI.TotientAsymptotic.prefix_budget_volume_lower line 16
  3. lemma OAI.TotientAsymptotic.ordered_translate_half_volume line 31
  4. theorem OAI.TotientAsymptotic.ordered_translate_volume line 68