OAI/NumberTheory/DirichletL/Moments/AddedZeroUniform.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.uniform_tuple_energy line 13
  2. abbrev OAI.SevenEighths.CenteredMomentAddedZeroUniform.Tuple line 42
  3. def OAI.SevenEighths.CenteredMomentAddedZeroUniform.coordinateEquiv line 44
  4. def OAI.SevenEighths.CenteredMomentAddedZeroUniform.tupleEquiv line 47
  5. def OAI.SevenEighths.CenteredMomentAddedZeroUniform.finiteTupleProduct line 51
  6. lemma OAI.SevenEighths.CenteredMomentAddedZeroUniform.tupleEquiv_slot line 53
  7. lemma OAI.SevenEighths.CenteredMomentAddedZeroUniform.tupleEquiv_plain line 61
  8. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.tupleProduct_reindex line 69
  9. def OAI.SevenEighths.CenteredMomentAddedZeroUniform.originalFiniteCoefficient line 74
  10. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.originalCoefficient_reindex line 83
  11. lemma OAI.SevenEighths.CenteredMomentAddedZeroUniform.reindex_supported line 98
  12. def OAI.SevenEighths.CenteredMomentAddedZeroUniform.finiteGaussZero line 106
  13. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.finiteGaussZero_reindex line 113
  14. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.uniform_finite_energy line 135
  15. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.originalFiniteCoefficient_norm_le line 156
  16. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.original_subset_energy line 176
  17. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.empty_finiteTupleProduct line 210
  18. lemma OAI.SevenEighths.CenteredMomentAddedZeroUniform.reindexCoefficient_mask line 219
  19. lemma OAI.SevenEighths.CenteredMomentAddedZeroUniform.reindexColumns_norm line 232
  20. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.finiteGaussZero_nonzero_mask_norm line 241
  21. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.finiteGaussZero_nonzero_mask_dyad line 252
  22. lemma OAI.SevenEighths.CenteredMomentAddedZeroUniform.originalFiniteCoefficient_mask line 265
  23. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.uniform_finite_source_energy line 273
  24. theorem OAI.SevenEighths.CenteredMomentAddedZeroUniform.original_subset_source_energy line 307