OAI/NumberTheory/CubicMoment/Estimates/LargeTupleOrdinaryScales.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The compactness grouping is converted to fixed smooth-box lengths. All constant support ratios are retained before the eventual power gap is used.

  1. lemma OAI.CubicFirstMoment.largePrimeTuplePiece_log_pos line 14
  2. theorem OAI.CubicFirstMoment.largePrimeTuplePiece_ordinary_group line 29