OAI/NumberTheory/CubicMoment/Theta/CubicThetaRowHeightEquation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every actual primitive row height, with arbitrary complex power, satisfies the hyperbolic spectral equation. This removes the nonzero cubic phase from the already proved literal grid equation.

  1. lemma OAI.CubicFirstMoment.cubicThetaGridTerm_row_height line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_const_mul line 18
  3. theorem OAI.CubicFirstMoment.cubicThetaRowHeightPower_eigenvalue line 24