OAI/Geometry/IsometricImmersion/Darboux/QResidualFactors.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.qCoordinateChainCoefficient line 12
  2. def OAI.SmoothLocal.HighEquation.qCoordinateChainFactor line 17
  3. def OAI.SmoothLocal.HighEquation.qFirstJetOffset line 21
  4. def OAI.SmoothLocal.HighEquation.qChainFactorOrder line 23
  5. theorem OAI.SmoothLocal.HighEquation.qFirstJetOffset_le_one line 26
  6. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainTerm_scalar_expansion line 29
  7. theorem OAI.SmoothLocal.HighEquation.coordinate_qSolutionJet_horizontal_positive line 35
  8. theorem OAI.SmoothLocal.HighEquation.q_residual_factor_orders line 51
  9. theorem OAI.SmoothLocal.HighEquation.q_residual_high_unique line 63
  10. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainFactor_continuousOn line 69
  11. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainProduct_continuousOn line 76
  12. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainCoefficient_continuousOn line 83
  13. theorem OAI.SmoothLocal.HighEquation.q_state_factor_low_bound line 99
  14. theorem OAI.SmoothLocal.HighEquation.q_state_factor_high_eLpNorm line 128