OAI/NumberTheory/DirichletL/Moments/ReflectionDeletion.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentReflectionDeletion.norm line 14
  2. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.norm_pos line 15
  3. def OAI.SevenEighths.CenteredMomentReflectionDeletion.outside line 17
  4. abbrev OAI.SevenEighths.CenteredMomentReflectionDeletion.SmoothIdeal line 18
  5. abbrev OAI.SevenEighths.CenteredMomentReflectionDeletion.OutsideIdeal line 19
  6. def OAI.SevenEighths.CenteredMomentReflectionDeletion.extract line 21
  7. def OAI.SevenEighths.CenteredMomentReflectionDeletion.residual line 23
  8. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.extract_factors line 25
  9. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.residual_factors line 29
  10. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.extract_ne_zero line 33
  11. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.residual_ne_zero line 36
  12. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.reconstruct line 39
  13. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.extract_smooth line 43
  14. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.outside_iff_factors line 49
  15. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.residual_outside line 56
  16. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.split_product line 61
  17. def OAI.SevenEighths.CenteredMomentReflectionDeletion.splitEquiv line 82
  18. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.outside_iff_coprime line 92
  19. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.deleted_coefficient line 110
  20. def OAI.SevenEighths.CenteredMomentReflectionDeletion.DecayTwo line 117
  21. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.schwartz_decayTwo line 119
  22. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.reflected_decayTwo line 125
  23. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.inverse_norm_sq_summable line 132
  24. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.radial_summable_norm line 139
  25. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.plain_summable line 149
  26. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.pair_radial_summable_norm line 157
  27. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.restricted_pair_summable line 169
  28. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.outside_plain_tsum line 181
  29. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.restoration_inner line 194
  30. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.restoration_plain_summable line 207
  31. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.restoration_plain line 214
  32. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.normalization_factor line 234
  33. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.normalized_restoration_term line 240
  34. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.normalized_restoration line 255
  35. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.reflected_normalized_restoration line 273
  36. def OAI.SevenEighths.CenteredMomentReflectionDeletion.outsideSum line 282
  37. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.outsideSum_summable line 285
  38. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.outside_mul_prime line 295
  39. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.prime_shift_tsum line 309
  40. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.outsideSum_insert line 353
  41. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.subset_product_nonzero line 373
  42. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.subset_product_norm_pos line 375
  43. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.finite_deletion_plain line 379
  44. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.normalized_dilation_term line 405
  45. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.normalized_finite_deletion line 420
  46. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.subset_product_moebius line 442
  47. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.normalized_finite_deletion_moebius line 452
  48. def OAI.SevenEighths.CenteredMomentReflectionDeletion.reflectedTerm line 463
  49. lemma OAI.SevenEighths.CenteredMomentReflectionDeletion.reflectedTerm_eq line 471
  50. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.deletion_reflection line 487
  51. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.primitive_deleted_reflection line 519
  52. theorem OAI.SevenEighths.CenteredMomentReflectionDeletion.primitive_deleted_reflection_absolute line 539