OAI/NumberTheory/TotientAsymptotic/StrictPrefixContraction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Diagonal contraction imposes strict Ford rows while preserving prime order.

  1. lemma OAI.TotientAsymptotic.prefixRegion_coordinate_nonneg line 12
  2. def OAI.TotientAsymptotic.contractedPrefix line 21
  3. lemma OAI.TotientAsymptotic.prefix_contraction line 26
  4. lemma OAI.TotientAsymptotic.prefix_contraction_gap line 78
  5. lemma OAI.TotientAsymptotic.reciprocal_enlargement_contracts line 93
  6. lemma OAI.TotientAsymptotic.reciprocal_enlargement_top line 102
  7. lemma OAI.TotientAsymptotic.contractedPrefix_subset_prefixRegion line 119
  8. lemma OAI.TotientAsymptotic.measurableSet_contractedPrefix line 129
  9. lemma OAI.TotientAsymptotic.ordered_prefix_contraction_volume line 163