OAI/NumberTheory/CubicMoment/Decomposition/StoppingMatrixLabels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Independent coefficient collection on any finite family of actual stopping labels, including the high-bin first-stage labels.

  1. theorem OAI.CubicFirstMoment.stopping_matrix_collection_on_labels line 12