OAI/NumberTheory/CubicMoment/Decomposition/StoppedModelOverlap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The coprimality loss for the actual early-stopped coefficients. Only nonzero rows need be rough; the ambient support is left unchanged.

  1. lemma OAI.CubicFirstMoment.bounded_noncoprime_row_sum line 14
  2. theorem OAI.CubicFirstMoment.stopped_model_overlap line 48