OAI/NumberTheory/CubicMoment/Angular/AngularStoppedMellinRows.lean

GitHub source file

3 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. def OAI.CubicFirstMoment.angularStoppedDivisorMass line 15
  2. lemma OAI.CubicFirstMoment.angularStoppedDivisorMass_eq line 22
  3. theorem OAI.CubicFirstMoment.angular_stopped_coprime_mellin_mass line 39