OAI/NumberTheory/CubicMoment/Decomposition/StoppingPrefixCrossing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact location of the first crossing relative to a bin boundary. This connects the manuscript's high-bin stage to the actual stopping labels, without imposing the boundary condition on the other variable.

  1. lemma OAI.CubicFirstMoment.selected_crossing_before_prefix_iff line 11
  2. lemma OAI.CubicFirstMoment.selected_crossing_after_prefix_iff line 28