OAI/NumberTheory/JointDickman/Counting/ArcCoefficientIdentity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The exact coefficient phase on a lifted major arc

  1. theorem OAI.JointDickman.additivePhase_int line 13
  2. theorem OAI.JointDickman.additivePhase_add_int line 19
  3. theorem OAI.JointDickman.finiteAdditiveSum_add_int line 22
  4. theorem OAI.JointDickman.finiteAdditiveSum_periodic line 30
  5. theorem OAI.JointDickman.lifted_arc_coefficient_phase line 35
  6. theorem OAI.JointDickman.coefficientExponentialSum_eq_smooth line 51

    Also declared: OAI/NumberTheory/JointDickman/Counting/LargeMajorCoefficient.lean:13 (same declaration text).

  7. theorem OAI.JointDickman.coefficientExponentialSum_neg_unit line 61
  8. theorem OAI.JointDickman.smoothCoefficientAdditiveSum_add_int line 74
  9. theorem OAI.JointDickman.lifted_arc_smooth_coefficient line 82