OAI/NumberTheory/Ostmann/Supply/PrimeBandSelectionBalance.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Supply.balancedDensityline 14 - theorem
OAI.Ostmann.Supply.log_ratio_lower_of_unbalancedline 17 - def
OAI.Ostmann.Supply.unbalancedPrimePrefixline 43 - theorem
OAI.Ostmann.Supply.unbalancedPrimePrefix_mass_leline 46