OAI/NumberTheory/TotientAsymptotic/NormalizedStrictSlack.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strict-slack slices remain negligible after summing the smooth cofactors.

  1. def OAI.TotientAsymptotic.normalizedStrictSlackLoss line 13
  2. lemma OAI.TotientAsymptotic.normalizedStrictSlackLoss_tendsto line 18
  3. theorem OAI.TotientAsymptotic.normalized_strict_slack_shell line 31