OAI/NumberTheory/TotientAsymptotic/HeavyOmegaMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed 15/8 moment needed for the large-Omega nice-value exception.

  1. def OAI.TotientAsymptotic.heavyOmegaReciprocal line 10
  2. lemma OAI.TotientAsymptotic.heavyOmegaReciprocal_nonneg line 23
  3. lemma OAI.TotientAsymptotic.heavyOmegaReciprocal_prime line 27
  4. lemma OAI.TotientAsymptotic.heavyOmegaReciprocal_norm line 31
  5. lemma OAI.TotientAsymptotic.heavy_omega_euler_log line 37
  6. lemma OAI.TotientAsymptotic.heavy_omega_euler_product line 58
  7. theorem OAI.TotientAsymptotic.heavy_omega_moment_bound line 84