OAI/NumberTheory/Ostmann/Supply/SquarefreeMultiplierCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An elementary positive-density supply of squarefree multipliers

  1. theorem OAI.Ostmann.reciprocal_square_step line 13
  2. theorem OAI.Ostmann.sum_reciprocal_squares_le_three_quarters line 23
  3. def OAI.Ostmann.nonSquarefreeMultipliers line 41
  4. def OAI.Ostmann.positiveMultiplesUpTo line 44
  5. theorem OAI.Ostmann.nonSquarefreeMultipliers_subset line 47
  6. theorem OAI.Ostmann.nonSquarefreeMultipliers_card_le line 66
  7. theorem OAI.Ostmann.nonSquarefreeMultipliers_real_card_le line 74