OAI/Geometry/TamingCompatibility/Hodge/HodgeLocalSmooth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.realEvaluation_smooth line 29
2. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationTerm_smooth_sum line 77
3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluation_smooth line 102
4. def OAI.TamingCompatibility.GeometricHilbert.hodgePreD line 129
5. def OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian line 134
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_apply line 139
7. lemma OAI.TamingCompatibility.GeometricHilbert.smoothL2_preD line 145
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_green_weak line 148
9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_green line 162
10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_nonnegative line 168
11. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_symmetric line 173
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_star line 186