OAI/NumberTheory/DirichletL/Moments/RetainedProfile.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentRetainedProfile.dilated line 14
  2. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.dilated_contDiff line 16
  3. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.dilated_support line 20
  4. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.seminorm_dilation_le line 35
  5. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.normPowerProfile_dilated line 62
  6. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.normPowerProfile_dilated_seminorm line 84
  7. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.normPowerProfile_dilated_finite line 99
  8. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.dilated_normPowerProfile_uniform_degree line 115
  9. def OAI.SevenEighths.CenteredMomentRetainedProfile.clippedScale line 143
  10. def OAI.SevenEighths.CenteredMomentRetainedProfile.clipDilation line 145
  11. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clippedScale_ge_one line 147
  12. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipDilation_ge_one line 149
  13. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipDilation_le line 153
  14. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipDilation_eq_one line 160
  15. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipDilation_subunit line 163
  16. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipped_source line 166
  17. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.strict_subunit_ideal_zero line 173
  18. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.strict_subunit_sum_zero line 183
  19. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipped_ideal_sum line 196
  20. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipped_twistedIdealSum line 204
  21. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.strict_subunit_twistedIdealSum_zero line 209
  22. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.clipped_rowTwistedSum line 215
  23. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.strict_subunit_rowTwistedSum_zero line 221
  24. def OAI.SevenEighths.CenteredMomentRetainedProfile.retainedProfile line 227
  25. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.retainedProfile_apply line 236
  26. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.retainedProfile_support line 243
  27. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.retainedProfile_uniform_degree line 252
  28. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.two_retainedProfile_uniform_degree line 266
  29. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.retained_row_rectangle line 293
  30. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.strict_subunit_row_rectangle_zero line 301
  31. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.two_retained_row_rectangles line 310
  32. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.two_retained_row_energies line 323
  33. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.retained_volumeControl_le line 357
  34. theorem OAI.SevenEighths.CenteredMomentRetainedProfile.retained_volumeControl_uniform_degree line 375