OAI/NumberTheory/DirichletL/Moments/FirstAmplifiedFourCoefficients.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.reference line 26
  2. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.mainCores line 28
  3. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.errorCores line 34
  4. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.lossVector line 42
  5. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.averagedCoefficients line 46
  6. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.actual_valuation_mass line 51
  7. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.actual_error_average line 54
  8. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.main_paid_core line 76
  9. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.error_paid_core line 91
  10. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.actual_main_cores line 114
  11. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.actual_error_cores line 199
  12. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.sourceCoefficients line 276
  13. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.shortened_power line 282
  14. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.source_coefficients_identity line 286
  15. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.averaged_coefficients_bound line 341
  16. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.actual_low_four_coefficients line 385
  17. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.source_normalized_identity line 432
  18. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.eventually_prime_average_gates line 461
  19. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.source_coefficients_nonneg line 473
  20. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.mainPowers line 495
  21. def OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.errorPowers line 498
  22. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.main_core_power line 502
  23. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.error_core_power line 509
  24. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedFourCoefficients.actual_power_reference_identity line 516