OAI/NumberTheory/CubicMoment/Estimates/LargeTuplePieceWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nonzero actual pieces provide all coordinate-envelope hypotheses. Thus no envelope admissibility is left as an extra analytic assumption.

  1. lemma OAI.CubicFirstMoment.largePrimeTuplePiece_witness line 13
  2. theorem OAI.CubicFirstMoment.eventually_largePrimeTuplePiece_high_full line 25