OAI/NumberTheory/CubicMoment/Decomposition/StoppingSupportCollection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Collection of the complete stopping sum, without assuming that the original term reaches the threshold. Its finite support stays exact.

  1. theorem OAI.CubicFirstMoment.geometricStoppedElement_support_collection line 12
  2. theorem OAI.CubicFirstMoment.finite_stopping_pair_split line 79