OAI/Geometry/TamingCompatibility/Hodge/HodgeRegularization.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationVector line 29
2. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationVector_continuous line 32
3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationVector_integrable line 36
4. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.regularize line 40
5. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.regularize_pair line 43
6. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.innerKernel line 50
7. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.innerKernel_continuous line 53
8. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.regularize_inner line 57
9. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.wedgeKernel line 66
10. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.wedgeKernel_continuous line 69
11. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.regularize_wedge line 73
12. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.regularize_add line 89
13. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.coordinate_basis_expansion line 115
14. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.basisForm_expansion line 135