OAI/Geometry/TamingCompatibility/Functional/MetricL2Completion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.PreL2 line 16
2. instance OAI.TamingCompatibility.GeometricHilbert.preL2Add line 19
3. instance OAI.TamingCompatibility.GeometricHilbert.preL2Module line 21
4. def OAI.TamingCompatibility.GeometricHilbert.preL2Core line 24
5. instance OAI.TamingCompatibility.GeometricHilbert.preL2Normed line 30
6. instance OAI.TamingCompatibility.GeometricHilbert.preL2Inner line 33
7. lemma OAI.TamingCompatibility.GeometricHilbert.preL2_inner line 36
8. lemma OAI.TamingCompatibility.GeometricHilbert.preL2_norm_sq line 40
9. abbrev OAI.TamingCompatibility.GeometricHilbert.L2 line 44
10. def OAI.TamingCompatibility.GeometricHilbert.smoothL2 line 46
11. lemma OAI.TamingCompatibility.GeometricHilbert.smoothL2_dense line 49