OAI/NumberTheory/CubicMoment/Decomposition/StoppedAllTuples.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The distinguished-role estimate for every finite tuple, including zero distinguished primes. The empty case is an exact vanishing identity.

  1. theorem OAI.CubicFirstMoment.stoppedBeta_distinguished_log_saving_all line 15