OAI/NumberTheory/CubicMoment/Decomposition/StoppedCharacterRows.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal stopped character sum as a squarefree coefficient row. The norm phase preserves its energy, and the energy is derived from the actual distinguished coefficient rather than supplied as a hypothesis.

  1. def OAI.CubicFirstMoment.stoppedIntervalSupport line 17
  2. def OAI.CubicFirstMoment.stoppedRowCoefficient line 23
  3. lemma OAI.CubicFirstMoment.stoppedIntervalSupport_spec line 30
  4. theorem OAI.CubicFirstMoment.stoppedCharacterSum_row line 40
  5. theorem OAI.CubicFirstMoment.stopped_interval_energy line 52