OAI/NumberTheory/TotientAsymptotic/LocalResidualExceptionData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Apply the exceptional estimates to the actual distinct suffix values.

  1. def OAI.TotientAsymptotic.localWitnessNonnormal line 15
  2. def OAI.TotientAsymptotic.localWitnessSquare line 18
  3. def OAI.TotientAsymptotic.localWitnessRegular line 22
  4. lemma OAI.TotientAsymptotic.local_regular_witness_properties line 25
  5. lemma OAI.TotientAsymptotic.local_residual_mass_partition line 43
  6. lemma OAI.TotientAsymptotic.local_residual_card_partition line 60
  7. lemma OAI.TotientAsymptotic.localNormalityScale_tendsto line 73
  8. theorem OAI.TotientAsymptotic.local_bad_suffix_exception_data line 77