OAI/Geometry/TamingCompatibility/Hodge/HodgeLocalEvaluation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.hodgeLocalizedRegularization line 24
2. structure OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing line 29
3. lemma OAI.TamingCompatibility.GeometricHilbert.exists_localHodgeSmoothing line 42
4. def OAI.TamingCompatibility.GeometricHilbert.localHodgeSmoothing line 67
5. def OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.evaluation line 76
6. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.evaluation_continuous line 80
7. def OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.representative line 84
8. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.evaluation_apply line 88
9. lemma OAI.TamingCompatibility.GeometricHilbert.LocalHodgeSmoothing.representative_spec line 92