OAI/Geometry/TamingCompatibility/Functional/GeometricCompact.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.smoothToChart line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.smoothToChart_dense line 26
3. lemma OAI.TamingCompatibility.GeometricHilbert.smoothToChart_metric_bound line 30
4. def OAI.TamingCompatibility.GeometricHilbert.chartToMetric line 39
5. lemma OAI.TamingCompatibility.GeometricHilbert.chartToMetric_smooth line 43
6. def OAI.TamingCompatibility.GeometricHilbert.energyInclusion line 48
7. def OAI.TamingCompatibility.GeometricHilbert.weakDelta line 51
8. lemma OAI.TamingCompatibility.GeometricHilbert.energyInclusion_injective line 54
9. lemma OAI.TamingCompatibility.GeometricHilbert.energyInclusion_factor line 58
10. theorem OAI.TamingCompatibility.GeometricHilbert.energyInclusion_compact line 72