OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelCanonical.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.gram_positive_definite line 12
2. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluation_eq line 33
3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationVector_eq line 46
4. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.innerKernel_eq line 50
5. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.wedgeKernel_eq line 54
6. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.regularize_eq line 58
7. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.innerKernel_symm line 63
8. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.wedgeKernel_symm line 66
9. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.innerKernel_positive_definite line 70