OAI/NumberTheory/TotientAsymptotic/HeadLimitedFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed upper cutoff for the leading tail coordinate costs vanishing volume.

  1. lemma OAI.TotientAsymptotic.renewalSeries_two_thirds_gt_one line 12
  2. lemma OAI.TotientAsymptotic.rho_lt_two_thirds line 23
  3. def OAI.TotientAsymptotic.headLimitedFamily line 31
  4. lemma OAI.TotientAsymptotic.measurableSet_headLimitedFamily line 34
  5. lemma OAI.TotientAsymptotic.geometric_family_subset_prefix line 40
  6. lemma OAI.TotientAsymptotic.head_cap_failure_is_coordinate_bad line 50
  7. theorem OAI.TotientAsymptotic.head_limited_volume_lower line 80