OAI/NumberTheory/Ostmann/Supply/KernelTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Supply.kernelDomain line 13
2. abbrev OAI.Ostmann.Supply.kernelCodomain line 16
3. def OAI.Ostmann.Supply.kernelTensor line 19
4. def OAI.Ostmann.Supply.kernelTensorPolynomial line 23
5. theorem OAI.Ostmann.Supply.eval_kernelTensorPolynomial line 27
6. theorem OAI.Ostmann.Supply.kernelTensor_norm_contraction line 35
7. theorem OAI.Ostmann.Supply.kernelTensor_norm_uniform line 47
8. theorem OAI.Ostmann.Supply.kernelTensor_point_pairing line 59