OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorCube.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Small square divisors act on the actual nonzero stopped rows. Zero coefficients impose no artificial coprimality condition on the ambient support.

  1. lemma OAI.CubicFirstMoment.divisorCubePoissonContribution_eq_of_active line 13
  2. lemma OAI.CubicFirstMoment.rough_coprime_small line 38
  3. lemma OAI.CubicFirstMoment.stopped_active_coprime_small line 47
  4. lemma OAI.CubicFirstMoment.stopped_divisor_cube_eq line 65