OAI/Geometry/TamingCompatibility/Hodge/HodgePatchAllCenters.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_zero_center line 24
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionResidual_zero_center line 38
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSliceForm_zero_center line 50
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSliceForm_zero_center line 62
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSliceForm_smooth_all line 74
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSliceForm_smooth_all line 83
7. def OAI.TamingCompatibility.ManifoldLocalization.squareMass line 105
8. lemma OAI.TamingCompatibility.ManifoldLocalization.squareMass_pos line 107
9. lemma OAI.TamingCompatibility.ManifoldLocalization.squareMass_smooth line 119
10. lemma OAI.TamingCompatibility.ManifoldLocalization.squareMass_inv_smooth line 122
11. lemma OAI.TamingCompatibility.ManifoldLocalization.squareMass_normalized line 125
12. lemma OAI.TamingCompatibility.HodgeFrame.pairing_basisForm line 138
13. lemma OAI.TamingCompatibility.HodgeFrame.basisForm_resolution line 146
14. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame line 164
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame_smooth line 169