OAI/NumberTheory/Ostmann/Supply/KernelEmpirical.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Supply.kernelCenteredDomain line 13
2. abbrev OAI.Ostmann.Supply.kernelCenteredCodomain line 14
3. def OAI.Ostmann.Supply.kernelOutputEmpirical line 16
4. def OAI.Ostmann.Supply.kernelInputEmpirical line 21
5. def OAI.Ostmann.Supply.kernelAverageWeight line 26
6. theorem OAI.Ostmann.Supply.kernelAverageWeight_nonneg line 31
7. theorem OAI.Ostmann.Supply.kernelEmpirical_pairing line 38
8. theorem OAI.Ostmann.Supply.kernelTruncation_lowMode_pairing line 71