OAI/NumberTheory/TotientAsymptotic/CoordinateCenters.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compare the center in a fixed truncated simplex with Ford's natural center.

  1. lemma OAI.TotientAsymptotic.truncated_center_factorization line 10
  2. lemma OAI.TotientAsymptotic.small_center_product line 22
  3. lemma OAI.TotientAsymptotic.truncated_center_bounds line 47