OAI/NumberTheory/TotientAsymptotic/CandidateNormalMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The normality prime-mass saving at the full-fiber construction's cutoff.

  1. def OAI.TotientAsymptotic.candidateNormalityScale line 14
  2. lemma OAI.TotientAsymptotic.candidateNormalityScale_gt_two line 16
  3. lemma OAI.TotientAsymptotic.candidateNormalityScale_factor line 22
  4. theorem OAI.TotientAsymptotic.candidate_non_normal_mass line 29
  5. lemma OAI.TotientAsymptotic.candidate_total_prime_mass line 63
  6. lemma OAI.TotientAsymptotic.candidate_prime_cutoff line 72