OAI/NumberTheory/CubicMoment/Theta/CubicThetaCenteredLow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Centering the actual completed transform with its now determined radial constant, at every fixed angular mode.

  1. lemma OAI.CubicFirstMoment.cubicThetaActualCompletedRadialMain_eq line 12
  2. theorem OAI.CubicFirstMoment.uniform_cubicTheta_centered_low line 18
  3. theorem OAI.CubicFirstMoment.uniform_cubicTheta_centered_subpower line 35