OAI/NumberTheory/DirichletL/Moments/ReflectedAnnuli.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow line 13
  2. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow_smooth line 15
  3. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow_support line 18
  4. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow_tsupport line 30
  5. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow_compact line 33
  6. def OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindowSchwartz line 36
  7. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow_derivative_window line 38
  8. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logWindow_derivative_bound line 48
  9. def OAI.SevenEighths.CenteredMomentReflectedAnnuli.reflected line 64
  10. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.reflected_smooth line 67
  11. def OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularProfile line 78
  12. def OAI.SevenEighths.CenteredMomentReflectedAnnuli.logProfile line 80
  13. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logProfile_apply line 86
  14. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logProfile_tsupport line 92
  15. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logProfile_finite_seminorm line 102
  16. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularProfile_support line 151
  17. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularProfile_zero line 160
  18. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annular_partition line 166
  19. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.normalized_annular_term line 175
  20. def OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass line 189
  21. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass_nonneg line 192
  22. lemma OAI.SevenEighths.CenteredMomentReflectedAnnuli.sqrt_nat_pow line 197
  23. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass_lower_bound line 203
  24. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass_upper_bound line 214
  25. lemma OAI.SevenEighths.CenteredMomentReflectedAnnuli.nonnegative_geometric_tail line 234
  26. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass_lower_tail line 245
  27. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass_upper_tail line 254
  28. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.annularMass_summable line 266
  29. theorem OAI.SevenEighths.CenteredMomentReflectedAnnuli.logProfile_dyadic_seminorm_sum line 271