OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothCommutation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_commute line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_cubes_commute line 30
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothInverse_commute line 36
4. def OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily line 45
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily_spec line 48
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily_graph line 53
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_twice_tendsto line 63
8. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationApply line 98
9. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationApply_smooth line 116
10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily_evaluation line 140
11. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily_twice_evaluation line 151
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily_uniform_tendsto line 163
13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothFamily_twice_uniform_tendsto line 179