OAI/NumberTheory/DirichletL/Moments/SourceMass.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentSourceMass.idealBall line 13
  2. theorem OAI.SevenEighths.CenteredMomentSourceMass.mem_idealBall line 17
  3. lemma OAI.SevenEighths.CenteredMomentSourceMass.idealBall_card line 26
  4. def OAI.SevenEighths.CenteredMomentSourceMass.tupleBox line 40
  5. lemma OAI.SevenEighths.CenteredMomentSourceMass.mem_tupleBox line 43
  6. lemma OAI.SevenEighths.CenteredMomentSourceMass.tupleBox_card line 47
  7. def OAI.SevenEighths.CenteredMomentSourceMass.profileProduct line 55
  8. lemma OAI.SevenEighths.CenteredMomentSourceMass.profileProduct_mem_box line 58
  9. lemma OAI.SevenEighths.CenteredMomentSourceMass.profileProduct_norm_le line 72
  10. theorem OAI.SevenEighths.CenteredMomentSourceMass.profileProduct_mass line 78
  11. def OAI.SevenEighths.CenteredMomentSourceMass.sourceProfiles line 104
  12. def OAI.SevenEighths.CenteredMomentSourceMass.sourceScales line 107
  13. def OAI.SevenEighths.CenteredMomentSourceMass.sourceBounds line 111
  14. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourceProfiles_product line 114
  15. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourceBounds_product line 128
  16. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourceScales_product line 134
  17. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourceBounds_nonneg line 141
  18. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourceScales_pos line 147
  19. theorem OAI.SevenEighths.CenteredMomentSourceMass.originalCoefficient_factor line 155
  20. def OAI.SevenEighths.CenteredMomentSourceMass.sourcePool line 168
  21. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourcePool_slot line 174
  22. lemma OAI.SevenEighths.CenteredMomentSourceMass.sourcePool_nonzero line 179
  23. theorem OAI.SevenEighths.CenteredMomentSourceMass.originalCoefficient_mem_sourcePool line 187
  24. def OAI.SevenEighths.CenteredMomentSourceMass.sourceRadius line 211
  25. lemma OAI.SevenEighths.CenteredMomentSourceMass.source_coordinate_product line 214
  26. lemma OAI.SevenEighths.CenteredMomentSourceMass.tupleBox_product_bound line 222
  27. theorem OAI.SevenEighths.CenteredMomentSourceMass.sourcePool_product_bound line 228
  28. theorem OAI.SevenEighths.CenteredMomentSourceMass.originalCoefficient_profile_norm_le line 237
  29. def OAI.SevenEighths.CenteredMomentSourceMass.sourceMassConstant line 263
  30. theorem OAI.SevenEighths.CenteredMomentSourceMass.originalCoefficient_mass line 266
  31. theorem OAI.SevenEighths.CenteredMomentSourceMass.sourcePool_original_slots line 310
  32. theorem OAI.SevenEighths.CenteredMomentSourceMass.tuple_weighted_regroup line 319
  33. theorem OAI.SevenEighths.CenteredMomentSourceMass.tupleCoefficient_mass line 334
  34. lemma OAI.SevenEighths.CenteredMomentSourceMass.tupleCoefficient_eq_zero_outside line 342
  35. theorem OAI.SevenEighths.CenteredMomentSourceMass.source_column_support line 349
  36. theorem OAI.SevenEighths.CenteredMomentSourceMass.original_source_eq_columns line 361
  37. lemma OAI.SevenEighths.CenteredMomentSourceMass.smooth_annular_bound line 384
  38. theorem OAI.SevenEighths.CenteredMomentSourceMass.smooth_source_mass_uniform line 398
  39. theorem OAI.SevenEighths.CenteredMomentSourceMass.originalCoefficient_original_masks line 449
  40. theorem OAI.SevenEighths.CenteredMomentSourceMass.originalCoefficient_product_bound line 466
  41. theorem OAI.SevenEighths.CenteredMomentSourceMass.sourceProfiles_annular_support line 482
  42. theorem OAI.SevenEighths.CenteredMomentSourceMass.sourcePool_prime_slots line 503
  43. def OAI.SevenEighths.CenteredMomentSourceMass.finiteColumns line 521
  44. def OAI.SevenEighths.CenteredMomentSourceMass.finiteColumnCoefficient line 524
  45. lemma OAI.SevenEighths.CenteredMomentSourceMass.finiteColumnCoefficient_mass line 528
  46. lemma OAI.SevenEighths.CenteredMomentSourceMass.finite_original_mass_reindex line 536
  47. theorem OAI.SevenEighths.CenteredMomentSourceMass.smooth_finite_source_mass_uniform line 549
  48. theorem OAI.SevenEighths.CenteredMomentSourceMass.smooth_subset_source_mass_uniform line 577
  49. theorem OAI.SevenEighths.CenteredMomentSourceMass.finiteColumns_reindex line 633
  50. theorem OAI.SevenEighths.CenteredMomentSourceMass.finiteColumnCoefficient_reindex line 641