OAI/NumberTheory/JointDickman/Amplification/SmallArcModel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The coefficient model on the retained denominator range

  1. def OAI.JointDickman.smallMajorArcModel line 12
  2. theorem OAI.JointDickman.smallArcSum_fourierModel line 20
  3. theorem OAI.JointDickman.smallMajorArc_energy_approximation line 61