OAI/NumberTheory/CubicMoment/Theta/CubicThetaDualIndex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full dual sum of the concrete core coefficient, with summability transferred from the proved arithmetic free-cube parametrization.

  1. lemma OAI.CubicFirstMoment.cubicThetaDualTerm_support line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaDualTerm_tsum line 27
  3. lemma OAI.CubicFirstMoment.cubicThetaDualTerm_summable_iff line 34
  4. theorem OAI.CubicFirstMoment.cubicThetaFullDual_voronoi line 45