OAI/NumberTheory/TwoPoint/Fourier/MajorArcEnergyRoot.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Taking the square root of the literal typical short energy. The first-band resolution losses are paid before character summation.

  1. lemma OAI.TwoPointCorrelations.major_arc_three_term_root line 10
  2. def OAI.TwoPointCorrelations.majorArcEnergyConstant line 23
  3. lemma OAI.TwoPointCorrelations.major_arc_energy_constant_pos line 26
  4. lemma OAI.TwoPointCorrelations.major_arc_short_energy_root line 31