OAI/NumberTheory/TotientAsymptotic/CoarseTotientBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coarse unconditional bounds used before the sharp counting-scale bootstrap.

  1. lemma OAI.TotientAsymptotic.V_nonneg line 12
  2. lemma OAI.TotientAsymptotic.V_le_self line 14
  3. lemma OAI.TotientAsymptotic.prime_counting_le_V line 21
  4. theorem OAI.TotientAsymptotic.V_coarse_lower line 43