OAI/Geometry/TamingCompatibility/Hodge/HodgeUnitKernelBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitFrameDirection_continuous line 23
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitFrameFunctional line 29
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitFrameFunctional_eq line 34
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitDual_encode line 46
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitFrameFunctional_continuous line 54
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitFrame_uniform line 67
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.currentFrame_bound line 77
8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitStarDirection line 112
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitStarDirection_continuous line 118
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitDual_star_encode line 124
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.wedgeFrame_bound line 137