OAI/Geometry/TamingCompatibility/Hodge/HodgeGlobalSmooth.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.GeometricHilbert.hodgeGraphResolvent_smooth line 21
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_injective line 55
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_injective line 71
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGraphResolvent_inclusion_power line 79
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_smooth line 92
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_cube_dense line 101
7. lemma OAI.TamingCompatibility.jAction_pairing line 128
8. def OAI.TamingCompatibility.GeometricHilbert.preJAction line 144
9. lemma OAI.TamingCompatibility.GeometricHilbert.preJAction_square line 154
10. def OAI.TamingCompatibility.GeometricHilbert.l2JAction line 158
11. lemma OAI.TamingCompatibility.GeometricHilbert.l2JAction_smooth line 163
12. lemma OAI.TamingCompatibility.GeometricHilbert.l2JAction_square line 169
13. lemma OAI.TamingCompatibility.GeometricHilbert.l2JAction_norm line 177
14. lemma OAI.TamingCompatibility.GeometricHilbert.l2JAction_self_adjoint line 184
15. def OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection line 191
16. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_apply line 194
17. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_smooth line 197
18. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_square line 203
19. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_self_adjoint line 209
20. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_norm line 214
21. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjectionStar line 221