OAI/Geometry/TamingCompatibility/Functional/RawNormal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricChart.normal_coordinateTest_at line 22
2. lemma OAI.TamingCompatibility.GeometricChart.rawScalar_smooth line 50
3. def OAI.TamingCompatibility.GeometricChart.rawPair line 55
4. lemma OAI.TamingCompatibility.GeometricChart.rawPair_smooth line 58
5. lemma OAI.TamingCompatibility.GeometricChart.normal_delta line 67
6. def OAI.TamingCompatibility.GeometricChart.normalOperator line 97
7. lemma OAI.TamingCompatibility.GeometricChart.normalOperator_zero_off line 101
8. lemma OAI.TamingCompatibility.GeometricChart.manifoldTest_delta_zero_off line 114
9. lemma OAI.TamingCompatibility.GeometricChart.normal_energy_point line 135
10. lemma OAI.TamingCompatibility.GeometricChart.normal_energy_integral line 149