OAI/NumberTheory/Ostmann/Supply/SmoothPrimeWeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.primeBump line 10
2. def OAI.Ostmann.Supply.primeWeight line 11
3. theorem OAI.Ostmann.Supply.primeWeight_contDiff line 13
4. theorem OAI.Ostmann.Supply.primeWeight_nonneg line 14
5. theorem OAI.Ostmann.Supply.primeWeight_le_one line 15
6. theorem OAI.Ostmann.Supply.primeWeight_compact line 16
7. theorem OAI.Ostmann.Supply.primeWeight_support line 18
8. theorem OAI.Ostmann.Supply.primeWeight_integral_pos line 26