OAI/NumberTheory/TotientAsymptotic/NormalBandAllocation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normality gives the factor-count caps required by the collision allocation bound.

  1. lemma OAI.TotientAsymptotic.omegaIn_upper_truncate line 11
  2. lemma OAI.TotientAsymptotic.normality_band_upper line 20
  3. lemma OAI.TotientAsymptotic.normal_band_product_omega line 46