OAI/Geometry/IsometricImmersion/Metrics/RemainderCoefficientBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.HighEquation.stateCompactTube_finite_P_bounds line 15
2. theorem OAI.SmoothLocal.HighEquation.coordinateChainCoefficient_abs_le_full_derivative line 34
3. theorem OAI.SmoothLocal.HighEquation.solutionJet_coord_bound_on_modelSquare line 44
4. theorem OAI.SmoothLocal.HighEquation.solutionJet_mem_compactTube_of_low_bound line 56
5. theorem OAI.SmoothLocal.HighEquation.exists_uniform_outer_remainder_coefficient_bound line 69
6. theorem OAI.SmoothLocal.HighEquation.exists_uniform_remainder_coefficients_original_data line 86
7. theorem OAI.SmoothLocal.HighEquation.exists_uniform_actualHighRemainder_bound_original_data line 110
8. theorem OAI.SmoothLocal.HighEquation.exists_uniform_actualHighRemainder_bound_frechet_data line 151