OAI/Geometry/IsometricImmersion/Comparison/ComparisonCoefficientSmooth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.comparisonStateMap line 15
2. def OAI.SmoothLocal.HighEquation.comparisonIntegrand line 18
3. def OAI.SmoothLocal.HighEquation.comparisonParameterDomain line 21
4. theorem OAI.SmoothLocal.HighEquation.comparisonStateMap_contDiffOn line 25
5. theorem OAI.SmoothLocal.HighEquation.comparisonParameterDomain_isOpen line 37
6. theorem OAI.SmoothLocal.HighEquation.comparisonIntegrand_contDiffOn line 44
7. theorem OAI.SmoothLocal.HighEquation.comparisonCoefficient_eq_parameterIntegral line 51
8. theorem OAI.SmoothLocal.HighEquation.comparisonCoefficient_contDiffOn line 59
9. theorem OAI.SmoothLocal.HighEquation.exists_comparison_coefficient_neighborhood line 72