OAI/NumberTheory/TotientAsymptotic/RoughIntervalMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Multiplicity-sensitive moments for the rough factors in a collision band.

  1. lemma OAI.TotientAsymptotic.rough_interval_weight_norm line 12
  2. lemma OAI.TotientAsymptotic.rough_interval_euler_log line 22
  3. lemma OAI.TotientAsymptotic.rough_interval_reciprocal_moment line 37