OAI/NumberTheory/TotientAsymptotic/PrefixGapWeights.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Signed simplex weights for an adjacent-coordinate gap.

  1. def OAI.TotientAsymptotic.prefixGapWeight line 10
  2. lemma OAI.TotientAsymptotic.prefix_gap_coordinate line 13
  3. theorem OAI.TotientAsymptotic.prefix_gap_weight_bounds line 23