OAI/Geometry/IsometricImmersion/Volterra/VolterraOperator.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.ODE.IntervalFunctions line 15
  2. def OAI.SmoothLocal.ODE.intervalExtension line 17
  3. theorem OAI.SmoothLocal.ODE.intervalExtension_apply_of_mem line 21
  4. theorem OAI.SmoothLocal.ODE.intervalExtension_norm_le line 27
  5. theorem OAI.SmoothLocal.ODE.intervalExtension_add line 33
  6. theorem OAI.SmoothLocal.ODE.intervalExtension_smul line 39
  7. def OAI.SmoothLocal.ODE.primitiveFunction line 43
  8. theorem OAI.SmoothLocal.ODE.primitiveFunction_continuous line 46
  9. theorem OAI.SmoothLocal.ODE.primitiveFunction_hasDerivAt line 51
  10. def OAI.SmoothLocal.ODE.primitiveMap line 59
  11. theorem OAI.SmoothLocal.ODE.primitiveMap_apply line 64
  12. def OAI.SmoothLocal.ODE.primitiveLinearMap line 68
  13. theorem OAI.SmoothLocal.ODE.primitiveMap_norm_le line 89
  14. def OAI.SmoothLocal.ODE.primitiveCLM line 105
  15. theorem OAI.SmoothLocal.ODE.primitiveCLM_apply line 110
  16. theorem OAI.SmoothLocal.ODE.primitiveCLM_norm_le line 114
  17. def OAI.SmoothLocal.ODE.volterraCLM line 118
  18. theorem OAI.SmoothLocal.ODE.volterraCLM_apply line 122
  19. theorem OAI.SmoothLocal.ODE.volterraCLM_norm_le line 134
  20. theorem OAI.SmoothLocal.ODE.volterraCLM_norm_le_one line 142