OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedRowsSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summed distinguished-coordinate cancellation. The total complementary mass is derived for the actual tuple weights and the actual norm cutoff.

  1. theorem OAI.CubicFirstMoment.stopped_distinguished_rows_saving line 14