OAI/NumberTheory/DirichletL/Moments/HeckeVolume.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentHeckeVolume.primaryCoefficient line 19
  2. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.primaryCoefficient_good line 28
  3. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.primaryCoefficient_norm line 34
  4. def OAI.SevenEighths.CenteredMomentHeckeVolume.periodicValue line 40
  5. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.periodicValue_mk line 43
  6. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.periodicValue_norm line 59
  7. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.lattice_eq_ideal_sum line 68
  8. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.fixed_period_volume line 98
  9. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.masked_hecke_volume line 115
  10. def OAI.SevenEighths.CenteredMomentHeckeVolume.fixedPeriod line 179
  11. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.fixedPeriod_ne_zero line 181
  12. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.fixedPeriod_three line 184
  13. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.span_fixedPeriod_le line 186
  14. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.inducedBy_of_elementCoeff_eq line 190
  15. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.fixedInducingRow_controlled line 214
  16. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.induced_primaryCoefficient line 230
  17. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.primaryCoefficient_actual_row line 239
  18. def OAI.SevenEighths.CenteredMomentHeckeVolume.density line 261
  19. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.density_norm_le line 267
  20. theorem OAI.SevenEighths.CenteredMomentHeckeVolume.actual_induced_volume line 299