OAI/Geometry/TamingCompatibility/DifferentialForms/SmoothingKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.HilbertKernel.kernel line 15
2. lemma OAI.TamingCompatibility.HilbertKernel.kernel_inner line 18
3. lemma OAI.TamingCompatibility.HilbertKernel.kernel_adjoint line 23
4. lemma OAI.TamingCompatibility.HilbertKernel.kernel_norm_le line 28
5. lemma OAI.TamingCompatibility.HilbertKernel.kernel_continuous line 33
6. def OAI.TamingCompatibility.HilbertKernel.regularize line 40
7. lemma OAI.TamingCompatibility.HilbertKernel.regularize_pair line 43
8. lemma OAI.TamingCompatibility.HilbertKernel.regularize_kernel_pair line 54
9. lemma OAI.TamingCompatibility.HilbertKernel.regularize_norm_sq line 67