OAI/Geometry/IsometricImmersion/Darboux/QSegmentAveraging.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.averagedQCoefficient line 14
2. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_fderiv_apply line 17
3. theorem OAI.SmoothLocal.HighEquation.qCoefficient_segment_continuousOn line 24
4. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_segment_FTC line 32
5. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_segment_FTC_of_jet_error line 71
6. theorem OAI.SmoothLocal.HighEquation.qHeightJetSegment_mean_linearization line 89
7. theorem OAI.SmoothLocal.HighEquation.averagedQCoefficient_lower line 120
8. theorem OAI.SmoothLocal.HighEquation.averagedQPrincipal_margin line 134