OAI/Geometry/IsometricImmersion/Taylor/TaylorPolynomialJetBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Taylor.normalizedTimePower_abs_le_one line 14
  2. theorem OAI.SmoothLocal.Taylor.normalizedTimePower_zero line 23
  3. theorem OAI.SmoothLocal.Taylor.normalizedTimePower_iteratedDeriv_abs_le_one line 27
  4. theorem OAI.SmoothLocal.Taylor.normalizedTimePower_fullJet_le_one line 40
  5. theorem OAI.SmoothLocal.Taylor.product_fullJet_bound line 45
  6. theorem OAI.SmoothLocal.Taylor.spatialCoefficient_fullJet_le line 68
  7. theorem OAI.SmoothLocal.Taylor.timeMonomial_fullJet_le_one line 78
  8. theorem OAI.SmoothLocal.Taylor.separatedTimePower_fullJet_bound line 89
  9. theorem OAI.SmoothLocal.Taylor.linearCauchy_fullJet_bound line 106