OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedNoStop.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The original distinguished subset weight itself is bounded by one. The no-stop estimate therefore applies to the complete small-product branch before any factor-count or prime-bin partition.

  1. lemma OAI.CubicFirstMoment.distinguishedSubsetWeight_norm_le_one line 17
  2. def OAI.CubicFirstMoment.distinguishedNoStopLow line 24
  3. theorem OAI.CubicFirstMoment.distinguishedNoStopLow_isLittleO line 32