OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternBulkMultiplier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retaining factors independent of the selected bulk draws

  1. theorem OAI.Ostmann.movingPatternBulkMean_weight line 10