OAI/Geometry/IsometricImmersion/Taylor/ScalarChainExpansion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.stateBaseOrder line 12
  2. theorem OAI.SmoothLocal.HighEquation.stateBaseOrder_le_two line 14
  3. theorem OAI.SmoothLocal.HighEquation.finite_state_basis_decomposition line 17
  4. theorem OAI.SmoothLocal.HighEquation.multilinear_state_components line 22
  5. def OAI.SmoothLocal.HighEquation.coordinateChainCoefficient line 41
  6. def OAI.SmoothLocal.HighEquation.coordinateChainFactor line 46
  7. def OAI.SmoothLocal.HighEquation.chainFactorOrder line 50
  8. theorem OAI.SmoothLocal.HighEquation.coordinateChainTerm_scalar_expansion line 53
  9. theorem OAI.SmoothLocal.HighEquation.solutionJetCurve_iteratedDeriv_positive line 60
  10. theorem OAI.SmoothLocal.HighEquation.coordinate_solutionJet_vertical_positive line 95
  11. theorem OAI.SmoothLocal.HighEquation.ChainWord.arity_le_total line 116
  12. theorem OAI.SmoothLocal.HighEquation.residual_scalar_factor_orders line 121
  13. theorem OAI.SmoothLocal.HighEquation.residual_scalar_high_unique line 133