OAI/Geometry/IsometricImmersion/Darboux/QHighEquation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.heightQCoefficient line 13
  2. def OAI.SmoothLocal.HighEquation.qDirectLinearization line 16
  3. def OAI.SmoothLocal.HighEquation.qSecondJetCorrection line 22
  4. def OAI.SmoothLocal.HighEquation.qFirstJetPairRemainder line 26
  5. def OAI.SmoothLocal.HighEquation.qCoordinateChainTerm line 30
  6. def OAI.SmoothLocal.HighEquation.qCoordinateChainSum line 34
  7. def OAI.SmoothLocal.HighEquation.actualQHighRemainder line 37
  8. theorem OAI.SmoothLocal.HighEquation.heightQCoefficient_contDiffOn line 41
  9. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_direction line 49
  10. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_zero_spatial_direction line 57
  11. theorem OAI.SmoothLocal.HighEquation.actualQ_top_chain_expansion line 65
  12. theorem OAI.SmoothLocal.HighEquation.actualQ_single_linearization line 86
  13. theorem OAI.SmoothLocal.HighEquation.second_fderiv_comp_constant_direction_xi line 96
  14. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_second_zero_spatial_direction line 113
  15. theorem OAI.SmoothLocal.HighEquation.actualQ_pair_extract_secondJet line 143
  16. theorem OAI.SmoothLocal.HighEquation.qChainTerm_eq_coordinateChainTerm line 175
  17. theorem OAI.SmoothLocal.HighEquation.qChainSum_eq_coordinateChainSum line 185
  18. theorem OAI.SmoothLocal.HighEquation.actual_differentiated_Q line 197
  19. def OAI.SmoothLocal.HighEquation.qHighBTheta line 222
  20. def OAI.SmoothLocal.HighEquation.qHighBXi line 225
  21. theorem OAI.SmoothLocal.HighEquation.actual_Q_hyperbolic_equation line 228