OAI/NumberTheory/CubicMoment/Angular/AngularStoppedCharacterRows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed-angular stopped coefficient and its exact character row. Angular multiplication preserves the proved pointwise and energy bounds; cube factors and divisor exclusions remain literal finite identities.

  1. def OAI.CubicFirstMoment.angularStoppedRowCoefficient line 16
  2. def OAI.CubicFirstMoment.angularStoppedCharacterSum line 20
  3. lemma OAI.CubicFirstMoment.angularStoppedRowCoefficient_norm line 25
  4. lemma OAI.CubicFirstMoment.angularStoppedCharacterSum_cube line 31
  5. lemma OAI.CubicFirstMoment.angularStoppedCharacterSum_divisibility line 49
  6. theorem OAI.CubicFirstMoment.angular_stopped_interval_energy line 63