OAI/Geometry/TamingCompatibility/Hodge/HodgeLocalKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.representative_on_test line 29
2. def OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.realEvaluation line 45
3. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.realEvaluation_continuous line 49
4. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.realEvaluation_apply line 53
5. def OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.regularizeLocal line 56
6. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.regularizeLocal_pair line 60
7. def OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.localKernel line 66
8. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.localKernel_continuous line 72
9. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.localKernel_adjoint line 78
10. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.regularizeLocal_kernel_pair line 84
11. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.realEvaluation_pair line 115