OAI/NumberTheory/CubicMoment/Estimates/TailHighCollection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of Gauss height-tail rows above any fixed scale threshold. This retains the independent smooth norm partitions and product envelope.

  1. def OAI.CubicFirstMoment.tailHighScaleRows line 15
  2. theorem OAI.CubicFirstMoment.tailHighScaleRows_arity line 19
  3. lemma OAI.CubicFirstMoment.tailHighScaleRows_window_split line 64