OAI/Geometry/IsometricImmersion/Volterra/VolterraGlue.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.ODE.prescribedLocalState line 15
  2. theorem OAI.SmoothLocal.ODE.prescribedLocalState_initial line 20
  3. theorem OAI.SmoothLocal.ODE.prescribedLocalState_hasDerivAt line 31
  4. theorem OAI.SmoothLocal.ODE.prescribedLocalState_agree line 49
  5. def OAI.SmoothLocal.ODE.interiorRadius line 82
  6. theorem OAI.SmoothLocal.ODE.interiorRadius_pos line 84
  7. theorem OAI.SmoothLocal.ODE.interiorRadius_lt_one line 88
  8. theorem OAI.SmoothLocal.ODE.abs_lt_interiorRadius line 92
  9. def OAI.SmoothLocal.ODE.globalPrescribedState line 96
  10. def OAI.SmoothLocal.ODE.globalPrescribedScalar line 99
  11. theorem OAI.SmoothLocal.ODE.globalPrescribedState_eq_local line 102
  12. theorem OAI.SmoothLocal.ODE.globalPrescribedScalar_contDiffOn line 114
  13. theorem OAI.SmoothLocal.ODE.globalPrescribedScalar_bounds line 132
  14. def OAI.SmoothLocal.ODE.prescribedFactor line 143
  15. theorem OAI.SmoothLocal.ODE.prescribedFactor_contDiffOn line 146
  16. theorem OAI.SmoothLocal.ODE.prescribedFactor_bounds line 154