OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicCalculus.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Periodic differentiation and integration on an open parameter domain.

  1. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.smooth_slice line 20
  2. def OAI.ClosedSurfaceR4.LocalPeriodicCalculus.bundleOn line 28
  3. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.bundleOn_apply line 35
  4. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.bundleOn_smooth line 41
  5. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.angle_smooth line 50
  6. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.slow_smooth line 55
  7. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.angle_hasDerivAt line 60
  8. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.fderiv_slice line 71
  9. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.periodic_angle line 83
  10. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.periodic_slow line 92
  11. def OAI.ClosedSurfaceR4.LocalPeriodicCalculus.angleOn line 102
  12. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.angleOn_hasDerivAt line 108
  13. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.angleOn_smooth line 115
  14. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.angleOn_zero_at line 120
  15. def OAI.ClosedSurfaceR4.LocalPeriodicCalculus.slowOn line 130
  16. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.slowOn_apply line 136
  17. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.slowOn_smooth line 143
  18. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.slowOn_zero_on line 149
  19. def OAI.ClosedSurfaceR4.LocalPeriodicCalculus.primitiveOn line 166
  20. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.primitiveOn_apply line 175
  21. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.primitiveOn_smooth line 182
  22. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.primitiveOn_hasDerivAt line 188
  23. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.primitiveOn_mean_zero line 195
  24. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.primitiveOn_zero_at line 204
  25. lemma OAI.ClosedSurfaceR4.LocalPeriodicCalculus.slowOn_mean_zero line 215