OAI/NumberTheory/JointDickman/Analysis/LaplaceBinShort.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite Laplace combinations have centered short averages

  1. theorem OAI.JointDickman.measurable_unitProgressionBinAverage line 11
  2. theorem OAI.JointDickman.unit_laplace_combination line 19
  3. theorem OAI.JointDickman.finite_complex_sum_energy line 41
  4. theorem OAI.JointDickman.unit_laplace_short_with_center line 69