OAI/Analysis/LipschitzHilbert/Fourier/SquareLineConcentration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Every-line BMO and moments of the positive packet square function.

  1. def OAI.LipschitzHilbert.LinePacketFamily.squareSum line 19
  2. def OAI.LipschitzHilbert.LinePacketFamily.shortSquare line 20
  3. def OAI.LipschitzHilbert.LinePacketFamily.longSquare line 22
  4. def OAI.LipschitzHilbert.LinePacketFamily.squareFunction line 24
  5. def OAI.LipschitzHilbert.LinePacketFamily.squareMeanConstant line 25
  6. theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_nonneg line 27
  7. theorem OAI.LipschitzHilbert.LinePacketFamily.shortSquare_nonneg line 30
  8. theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_continuous line 33
  9. theorem OAI.LipschitzHilbert.LinePacketFamily.shortSquare_continuous line 36
  10. theorem OAI.LipschitzHilbert.LinePacketFamily.longSquare_continuous line 45
  11. theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_split line 54
  12. theorem OAI.LipschitzHilbert.LinePacketFamily.longSquare_oscillation line 64
  13. theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_mean_oscillation line 74
  14. theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_root_integral line 108
  15. theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_mean line 129
  16. theorem OAI.LipschitzHilbert.LinePacketFamily.squareFunction_moment line 144