OAI/NumberTheory/CubicMoment/Decomposition/StoppingFailedPair.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The late-stage failure condition is exactly a predicate on the selected divisor, even before restricting the original support.

  1. lemma OAI.CubicFirstMoment.stoppedSideTest_late_boundary line 12
  2. theorem OAI.CubicFirstMoment.stoppedSideTest_failed_pair_iff line 28