OAI/NumberTheory/JointDickman/Counting/ShortWindowEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Mean-square control of short windows by a nonnegative long mean

  1. def OAI.JointDickman.shortWindowEnergy line 10
  2. theorem OAI.JointDickman.shortWindowEnergy_integrable line 13
  3. theorem OAI.JointDickman.shortWindowEnergy_integral_le line 22
  4. theorem OAI.JointDickman.shortWindowEnergy_eq line 42
  5. theorem OAI.JointDickman.short_interval_card_le line 58
  6. theorem OAI.JointDickman.complexShortAverage_sq_le_window line 65
  7. theorem OAI.JointDickman.complexShortAverage_energy_le_prefix line 90