OAI/NumberTheory/JointDickman/Counting/ComplexFiniteShortAverages.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite complex combinations of nonprincipal short averages

  1. theorem OAI.JointDickman.PublishedInputs.measurable_complexShortAverage line 11
  2. theorem OAI.JointDickman.PublishedInputs.norm_complexShortAverage_le line 17
  3. theorem OAI.JointDickman.PublishedInputs.complexShortAverage_sq_integrable line 31
  4. def OAI.JointDickman.PublishedInputs.complexFiniteShort line 42
  5. theorem OAI.JointDickman.PublishedInputs.complexFiniteShort_norm_sq_le line 46
  6. theorem OAI.JointDickman.PublishedInputs.complexFiniteShort_energy_le line 55
  7. theorem OAI.JointDickman.PublishedInputs.complexFiniteShort_eventually_eventually line 77