OAI/NumberTheory/TotientAsymptotic/PrimeGridLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive prime mass in grids with a large reverse linear lower envelope.

  1. lemma OAI.TotientAsymptotic.sum_exp_neg_linear_prefix_sharp line 12
  2. theorem OAI.TotientAsymptotic.grid_prime_mass_lower line 51