OAI/NumberTheory/DirichletL/Descent/Overlap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.InverseMoment.moebius_squarefree_sq line 16
  2. theorem OAI.SevenEighths.InverseMoment.moebius_overlap_recovery line 21
  3. theorem OAI.SevenEighths.InverseMoment.moebius_character_overlap line 25
  4. theorem OAI.SevenEighths.InverseMoment.hybrid_mask_quotients line 35
  5. theorem OAI.SevenEighths.InverseMoment.inverse_eq_square_of_fourth_eq line 59
  6. theorem OAI.SevenEighths.InverseMoment.inverse_cube_square_eq_sixth line 73
  7. theorem OAI.SevenEighths.InverseMoment.inverse_square_cube_mask line 79
  8. theorem OAI.SevenEighths.InverseMoment.overlap_scalar_norm_le line 85