PrimeStoppingCollection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite reindexing from choices in the stopping bin to the independent selected and complementary divisor subsets.

def OAI.CubicFirstMoment.stoppingDivisorSubsets line 12
theorem OAI.CubicFirstMoment.stopping_subset_sum line 20
Source documentation
This is the finite reindexing behind independent alpha/beta collection; both subsets, and hence all coefficient weights, are exact.
```
theorem stopping_subset_sum (s : Finset Eisenstein) (bin : Eisenstein → ℕ)
    (j k : ℕ) (K : Finset Eisenstein → Finset Eisenstein → ℂ) :
    (∑ t ∈ (primeBin s bin j).powersetCard k,
      K (stoppingSelected s bin j t) (stoppingRemainder s bin j t)) =
    ∑ d ∈ stoppingDivisorSubsets s bin j k, K d (s \ d) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.stoppingRemainder, OAI.CubicFirstMoment.stoppingDivisorSubsets