OAI/NumberTheory/CubicMoment/Decomposition/StoppedMellinRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two actual coprime Poisson rows are the literal stopped rows at the shifted norm heights. Divisibility filters and the original interval support remain in the statement.

  1. lemma OAI.CubicFirstMoment.stoppedRowCoefficient_phase line 15
  2. def OAI.CubicFirstMoment.stoppedDivisorMass line 22
  3. lemma OAI.CubicFirstMoment.stoppedDivisorMass_eq line 29
  4. theorem OAI.CubicFirstMoment.stopped_coprime_mellin_mass line 46