OAI/NumberTheory/Ostmann/Preliminaries/WindowMass.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Preliminaries.eventually_upperWindow_card_lowerline 11 - def
OAI.Ostmann.Preliminaries.uniformWindowMassline 46 - theorem
OAI.Ostmann.Preliminaries.uniformWindowMass_nonnegline 49 - theorem
OAI.Ostmann.Preliminaries.uniformWindowMass_sumline 52 - theorem
OAI.Ostmann.Preliminaries.eventually_uniformWindowMass_capline 57