OAI/NumberTheory/DirichletL/Descent/ActualProfiles.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMoment.inverseNormWindow line 10
  2. def OAI.SevenEighths.InverseMoment.inverseRootWindow line 11
  3. def OAI.SevenEighths.InverseMoment.firstRootWindows line 13
  4. def OAI.SevenEighths.InverseMoment.firstLeftSlope line 17
  5. def OAI.SevenEighths.InverseMoment.firstRightSlope line 18
  6. def OAI.SevenEighths.InverseMoment.firstKernelSlope line 19
  7. def OAI.SevenEighths.InverseMoment.secondRootWindows line 21
  8. def OAI.SevenEighths.InverseMoment.secondLeftSlope line 25
  9. def OAI.SevenEighths.InverseMoment.secondRightSlope line 26
  10. def OAI.SevenEighths.InverseMoment.secondKernelSlope line 27
  11. def OAI.SevenEighths.InverseMoment.firstPoissonProfile line 29
  12. def OAI.SevenEighths.InverseMoment.secondPoissonProfile line 36
  13. def OAI.SevenEighths.InverseMoment.profileMode line 43
  14. theorem OAI.SevenEighths.InverseMoment.first_profile_common_measure line 48
  15. theorem OAI.SevenEighths.InverseMoment.second_profile_common_measure line 74