OAI/NumberTheory/DirichletL/Moments/FullCorrelation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentCorrelation.scaledResidue line 11
  2. theorem OAI.SevenEighths.CenteredMomentCorrelation.scaledResidue_mk line 24
  3. def OAI.SevenEighths.CenteredMomentCorrelation.fullModulusCorrelation line 28
  4. theorem OAI.SevenEighths.CenteredMomentCorrelation.scaledResidue_congruence line 36
  5. theorem OAI.SevenEighths.CenteredMomentCorrelation.fullModulusCorrelation_fourier line 45
  6. theorem OAI.SevenEighths.CenteredMomentCorrelation.common_divisor_frequency line 58
  7. theorem OAI.SevenEighths.CenteredMomentCorrelation.fullModulusCorrelation_eq_zero_of_common_not_dvd line 66
  8. theorem OAI.SevenEighths.CenteredMomentCorrelation.dvd_of_unit_residue_mul line 86
  9. theorem OAI.SevenEighths.CenteredMomentCorrelation.zero_frequency_units_force_divides line 96
  10. theorem OAI.SevenEighths.CenteredMomentCorrelation.fullModulusCorrelation_zero_frequency_off_diagonal line 108
  11. theorem OAI.SevenEighths.CenteredMomentCorrelation.scaledResidue_injective line 151
  12. theorem OAI.SevenEighths.CenteredMomentCorrelation.fullModulusCorrelation_zero_frequency_diagonal line 163