OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFourierPhase.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact additive phase separation on the triangularized branches. The finite character has the same codifferent and sign as the original horizontal Fourier expansion.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeFourierPhase line 12