OAI/NumberTheory/TwoPoint/Walks/CanonicalRetainedMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The retained divisor bins carry at least half the original harmonic mass, and the exact tuple mass is at least W^J.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_retained_mass line 14