OAI/NumberTheory/CubicMoment/Theta/CubicThetaFreeLocalVoronoi.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete angular transform with the free cube variable separated. Both its coefficient bound and its absolutely convergent sum are proved.

  1. def OAI.CubicFirstMoment.cubicThetaCommonArgument line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaCommonArgument_injective line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaLocalDualTerm_reindex line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaCoreCoefficient_index line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaFreeCubeJoin_argument line 41
  6. def OAI.CubicFirstMoment.cubicThetaFreeLocalDualTerm line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaFreeLocalDualTerm_eq line 65
  8. theorem OAI.CubicFirstMoment.cubicThetaFree_voronoi line 80