OAI/Geometry/TamingCompatibility/Hodge/HodgeBoundedSection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.scalar_pair_add line 27
2. lemma OAI.TamingCompatibility.GeometricHilbert.scalar_pair_smul line 38
3. def OAI.TamingCompatibility.GeometricHilbert.scalarSectionFunctional line 48
4. def OAI.TamingCompatibility.GeometricHilbert.boundedScalarSection line 63
5. lemma OAI.TamingCompatibility.GeometricHilbert.boundedScalarSection_norm line 71
6. lemma OAI.TamingCompatibility.GeometricHilbert.boundedScalarSection_pairing line 83
7. lemma OAI.TamingCompatibility.GeometricHilbert.boundedScalarSection_unique line 96
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMassBound_exists line 129
9. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMassBound line 133
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMassBound_nonneg line 135
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMassBound_bound line 137
12. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFramePreL2 line 141
13. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameCoefficient line 144
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameCoefficient_measurable line 148
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameCoefficient_bound line 155
16. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.boundedFrameSection line 163
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.boundedFrameSection_norm line 172
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_coefficient_sum line 190
19. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.boundedFrameSection_pairing line 205