OAI/NumberTheory/CubicMoment/Angular/AngularStoppedModelOverlap.lean

GitHub source file

1 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. theorem OAI.CubicFirstMoment.angular_stopped_model_overlap line 18