OAI/NumberTheory/CubicMoment/Decomposition/StoppedRowBinShift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal stopped beta on a dilated norm envelope is the existing analytic row after the exact shift of descending geometric bin labels. The cutoff parameters and every selected-side condition remain unchanged.

  1. theorem OAI.CubicFirstMoment.stoppedBeta_geometric_eq_row line 15