OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialDual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The radial dual sum uses the same proved local support and free-cube reindexing as the angular formula. Its separate actual pole is retained.

  1. theorem OAI.CubicFirstMoment.cubicThetaFullDual_radial_voronoi line 13