OAI/NumberTheory/Ostmann/Supply/CenteredBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.boundedSupportWeight line 13
2. theorem OAI.Ostmann.Supply.boundedSupportWeight_pos line 16
3. theorem OAI.Ostmann.Supply.primeProduct_boundedSupportWeight line 24
4. theorem OAI.Ostmann.Supply.primitiveEnergy_centered_expansion_bounded line 31
5. theorem OAI.Ostmann.Supply.sum_primitiveEnergy_squarefree_le line 43
6. theorem OAI.Ostmann.Supply.centered_energy_sum_le line 57
7. theorem OAI.Ostmann.Supply.sample_card_le_of_log_budget line 98