OAI/NumberTheory/DirichletL/Moments/ZeroMode.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentZeroMode.pairResidue_mul line 16
  2. theorem OAI.SevenEighths.CenteredMomentZeroMode.pairFourier_zero line 26
  3. theorem OAI.SevenEighths.CenteredMomentZeroMode.pairResidue_unit_eq_one_of_mean_ne_zero line 31
  4. theorem OAI.SevenEighths.CenteredMomentZeroMode.rows_agree_of_mean_ne_zero line 45
  5. theorem OAI.SevenEighths.CenteredMomentZeroMode.valuation_profile_of_mean_ne_zero line 65
  6. theorem OAI.SevenEighths.CenteredMomentZeroMode.powerful_product_of_mean_ne_zero line 77
  7. theorem OAI.SevenEighths.CenteredMomentZeroMode.powerful_pair_count line 92
  8. theorem OAI.SevenEighths.CenteredMomentZeroMode.pairFourier_zero_norm_le line 134
  9. theorem OAI.SevenEighths.CenteredMomentZeroMode.scaled_zero_mean_norm_le line 152
  10. theorem OAI.SevenEighths.CenteredMomentZeroMode.nonzero_mean_pair_count line 167
  11. theorem OAI.SevenEighths.CenteredMomentZeroMode.first_zero_sum_bound line 193
  12. theorem OAI.SevenEighths.CenteredMomentZeroMode.productColumnCoefficient_sextic_row_sum line 234
  13. theorem OAI.SevenEighths.CenteredMomentZeroMode.productColumnCoefficient_small_power line 250
  14. def OAI.SevenEighths.CenteredMomentZeroMode.idealColumn line 262
  15. theorem OAI.SevenEighths.CenteredMomentZeroMode.idealColumn_span line 265
  16. theorem OAI.SevenEighths.CenteredMomentZeroMode.idealColumn_supported line 269
  17. def OAI.SevenEighths.CenteredMomentZeroMode.idealZeroEnergy line 275
  18. theorem OAI.SevenEighths.CenteredMomentZeroMode.ideal_zero_energy_bound line 282
  19. theorem OAI.SevenEighths.CenteredMomentZeroMode.productColumnCoefficient_norm_le line 316
  20. theorem OAI.SevenEighths.CenteredMomentZeroMode.productColumns_supported line 331
  21. def OAI.SevenEighths.CenteredMomentZeroMode.productZeroEnergy line 339
  22. theorem OAI.SevenEighths.CenteredMomentZeroMode.product_zero_energy_bound line 345
  23. theorem OAI.SevenEighths.CenteredMomentZeroMode.normalized_product_zero_energy_bound line 383
  24. theorem OAI.SevenEighths.CenteredMomentZeroMode.aggregated_rowPolynomial line 404
  25. theorem OAI.SevenEighths.CenteredMomentZeroMode.aggregated_rowEnergy line 417
  26. theorem OAI.SevenEighths.CenteredMomentZeroMode.idealZeroEnergy_first_frequency line 426
  27. theorem OAI.SevenEighths.CenteredMomentZeroMode.normalized_product_zero_mode_bound line 439