OAI/Geometry/SurfaceImmersion/Correction/SmoothPeriodicCalculus.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Canonical periodic primitives and angular derivatives in a smooth family.

  1. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angleDerivative line 21
  2. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.contDiff_angleDerivative line 24
  3. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angle_hasDerivAt line 28
  4. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.bundle line 37
  5. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.bundle_apply line 41
  6. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.bundleFamily line 44
  7. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.bundleFamily_apply line 49
  8. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.periodic_angleDerivative line 53
  9. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.periodic_lift line 62
  10. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.derivativeFamily line 68
  11. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.derivativeFamily_hasDerivAt line 73
  12. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.derivativeFamily_smooth line 78
  13. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.derivativeFamily_mean_zero line 85
  14. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.primitiveFamily line 96
  15. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.primitiveFamily_apply line 104
  16. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.primitiveFamily_smooth line 109
  17. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.primitiveFamily_hasDerivAt line 115
  18. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.primitiveFamily_mean_zero line 121
  19. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.derivativeFamily_primitiveFamily line 128