OAI/NumberTheory/DirichletL/Moments/AddedZero.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentAddedZero.supported_one_ideal line 18
  2. lemma OAI.SevenEighths.CenteredMomentAddedZero.supported_one_element line 23
  3. theorem OAI.SevenEighths.CenteredMomentAddedZero.pairFourier_one line 26
  4. theorem OAI.SevenEighths.CenteredMomentAddedZero.gaussRow_zero_sixthRemainder line 49
  5. theorem OAI.SevenEighths.CenteredMomentAddedZero.gaussRow_zero_ideal_sixth_power line 68
  6. theorem OAI.SevenEighths.CenteredMomentAddedZero.gaussRow_norm_le line 74
  7. theorem OAI.SevenEighths.CenteredMomentAddedZero.squarefree_divisor_sixth_of_gauss_zero line 81
  8. def OAI.SevenEighths.CenteredMomentAddedZero.idealGaussRow line 89
  9. lemma OAI.SevenEighths.CenteredMomentAddedZero.idealGaussRow_norm_le line 92
  10. lemma OAI.SevenEighths.CenteredMomentAddedZero.idealGaussRow_zero_sixthRemainder line 97
  11. def OAI.SevenEighths.CenteredMomentAddedZero.tupleProduct line 103
  12. lemma OAI.SevenEighths.CenteredMomentAddedZero.tupleEntry_dvd line 105
  13. theorem OAI.SevenEighths.CenteredMomentAddedZero.tuple_product_fiber_card line 108
  14. def OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero line 124
  15. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_norm_le line 128
  16. def OAI.SevenEighths.CenteredMomentAddedZero.normalizedIdealAddedZero line 162
  17. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_energy line 165
  18. def OAI.SevenEighths.CenteredMomentAddedZero.tupleCoefficient line 191
  19. def OAI.SevenEighths.CenteredMomentAddedZero.tupleColumns line 195
  20. lemma OAI.SevenEighths.CenteredMomentAddedZero.tupleColumns_supported line 198
  21. theorem OAI.SevenEighths.CenteredMomentAddedZero.tupleCoefficient_norm_le line 205
  22. theorem OAI.SevenEighths.CenteredMomentAddedZero.tuple_added_zero_energy line 220
  23. def OAI.SevenEighths.CenteredMomentAddedZero.originalCoefficient line 269
  24. lemma OAI.SevenEighths.CenteredMomentAddedZero.idealRectangle_norm_le line 280
  25. theorem OAI.SevenEighths.CenteredMomentAddedZero.originalCoefficient_norm_le line 293
  26. lemma OAI.SevenEighths.CenteredMomentAddedZero.originalCoefficient_eq_zero_of_not_dvd line 322
  27. theorem OAI.SevenEighths.CenteredMomentAddedZero.original_added_zero_energy line 330
  28. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_eq_gaussPolynomial line 355
  29. lemma OAI.SevenEighths.CenteredMomentAddedZero.idealGaussRow_zero_divisor_sixth line 363
  30. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_nonzero_mask_norm line 372
  31. theorem OAI.SevenEighths.CenteredMomentAddedZero.original_tupleCoefficient_mask line 388
  32. theorem OAI.SevenEighths.CenteredMomentAddedZero.added_zero_exponent line 400
  33. theorem OAI.SevenEighths.CenteredMomentAddedZero.added_zero_scale_identity line 403
  34. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_source_energy line 409
  35. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_nonzero_mask_dyad line 427
  36. theorem OAI.SevenEighths.CenteredMomentAddedZero.idealAddedZero_source_energy_of_mask line 445
  37. theorem OAI.SevenEighths.CenteredMomentAddedZero.actual_tuple_gauss_eq_columns line 460