OAI/Geometry/NearbyLagrangian/Superposition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth superposition on continuous paths and Volterra integration.

  1. def OAI.NearbyLagrangian.SmoothFlow.pointwiseLinear line 19
  2. lemma OAI.NearbyLagrangian.SmoothFlow.pointwiseLinear_apply line 31
  3. def OAI.NearbyLagrangian.SmoothFlow.pointwiseOperator line 34
  4. lemma OAI.NearbyLagrangian.SmoothFlow.pointwiseOperator_apply line 49
  5. lemma OAI.NearbyLagrangian.SmoothFlow.uniform_zero_radius line 54
  6. theorem OAI.NearbyLagrangian.SmoothFlow.hasFDerivAt_superposition line 69
  7. theorem OAI.NearbyLagrangian.SmoothFlow.contDiff_superposition_nat line 106
  8. theorem OAI.NearbyLagrangian.SmoothFlow.contDiff_superposition line 121
  9. abbrev OAI.NearbyLagrangian.SmoothFlow.UnitTime line 132
  10. def OAI.NearbyLagrangian.SmoothFlow.pathExtend line 135
  11. lemma OAI.NearbyLagrangian.SmoothFlow.continuous_pathExtend line 138
  12. lemma OAI.NearbyLagrangian.SmoothFlow.pathExtend_coe line 142
  13. lemma OAI.NearbyLagrangian.SmoothFlow.norm_pathExtend_le line 146
  14. def OAI.NearbyLagrangian.SmoothFlow.volterra line 149
  15. lemma OAI.NearbyLagrangian.SmoothFlow.volterra_apply line 178
  16. lemma OAI.NearbyLagrangian.SmoothFlow.norm_volterra_le line 181