OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedDirichletCube.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual ramified cube step with its three low rows retained. Their residues must be determined; this identity does not assume that they vanish or that the full residue is cube-periodic.

  1. def OAI.CubicFirstMoment.cubicThetaRamifiedLowDirichlet line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_ramified_cube line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaRamifiedLowDirichlet_primary line 39