OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact shortening for a divisor-restricted stopped row. The shortened coefficient remains the original coefficient evaluated at d*n; no new prime-factor independence is asserted.

  1. def OAI.CubicFirstMoment.stoppedDivisorSlice line 14
  2. lemma OAI.CubicFirstMoment.stoppedDivisorSlice_spec line 19
  3. lemma OAI.CubicFirstMoment.stoppedDivisorSlice_complete line 27
  4. theorem OAI.CubicFirstMoment.stopped_divisor_sum_eq_slice line 37
  5. theorem OAI.CubicFirstMoment.stopped_divisor_character_sum line 55
  6. theorem OAI.CubicFirstMoment.stopped_divisor_character_norm_le line 69
  7. theorem OAI.CubicFirstMoment.stopped_slice_energy line 79