OAI/NumberTheory/TotientAsymptotic/LocalNormalityDiscard.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summation of all local normality failures in the actual candidate grid.

  1. def OAI.TotientAsymptotic.localNormalityFailures line 13
  2. theorem OAI.TotientAsymptotic.local_normality_discard line 17