OAI/Geometry/IsometricImmersion/Taylor/TaylorSeparatedProduct.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Taylor.spatialStrip line 13
  2. theorem OAI.SmoothLocal.Taylor.spatialStrip_isOpen line 15
  3. def OAI.SmoothLocal.Taylor.separatedProduct line 18
  4. theorem OAI.SmoothLocal.Taylor.separatedProduct_contDiffOn line 20
  5. theorem OAI.SmoothLocal.Taylor.initialPoint_hasDerivAt line 26
  6. theorem OAI.SmoothLocal.Taylor.point_eta line 34
  7. theorem OAI.SmoothLocal.Taylor.separatedProduct_partial_x line 38
  8. theorem OAI.SmoothLocal.Taylor.separatedProduct_partial_t line 55
  9. def OAI.SmoothLocal.Taylor.taylorCorrection line 71
  10. theorem OAI.SmoothLocal.Taylor.taylorCorrection_contDiffOn line 74
  11. theorem OAI.SmoothLocal.Taylor.taylorCorrection_partial_x line 79
  12. theorem OAI.SmoothLocal.Taylor.taylorCorrection_partial_t line 86
  13. theorem OAI.SmoothLocal.Taylor.taylorCorrection_partial_xx line 96
  14. theorem OAI.SmoothLocal.Taylor.taylorCorrection_partial_xt line 109
  15. theorem OAI.SmoothLocal.Taylor.taylorCorrection_partial_tt line 121
  16. theorem OAI.SmoothLocal.Taylor.taylorCorrection_tt_time_jet line 135