OAI/NumberTheory/CubicMoment/Estimates/SquarefreeTypeIMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The coefficient mass for the actual squarefree Type-I outer levels. Only the primary-prime theorem enters the divisor moment.

  1. lemma OAI.CubicFirstMoment.squarefree_primary_divisor_card_le line 12
  2. theorem OAI.CubicFirstMoment.squarefree_typeI_coefficient_mass line 18