OAI/Geometry/SurfaceImmersion/Primitive/PeriodicFamilies.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Smooth periodic families used in the finite metric expansion.

  1. def OAI.ClosedSurfaceR4.PeriodicExpansion.smoothFamilies line 17
  2. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family line 31
  3. instance OAI.ClosedSurfaceR4.PeriodicExpansion.(instance at line 33) line 33
  4. instance OAI.ClosedSurfaceR4.PeriodicExpansion.(instance at line 35) line 35
  5. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.val line 42
  6. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.smooth line 44
  7. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.ext line 47
  8. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.zero_apply line 52
  9. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.add_apply line 53
  10. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.neg_apply line 55
  11. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.sub_apply line 57
  12. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.smul_apply line 59
  13. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.sum_apply line 62
  14. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.slow line 69
  15. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.angle line 72
  16. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.slow_apply line 75
  17. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.angle_apply line 79
  18. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.primitive line 85
  19. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.primitive_angle line 88
  20. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.primitive_mean_zero line 93
  21. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.slow_mean_zero line 97
  22. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.inner line 100
  23. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.inner_apply line 105
  24. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.constant line 112
  25. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.constant_apply line 115
  26. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.mean line 120
  27. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct line 123
  28. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.mean_apply line 125
  29. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct_apply line 128
  30. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct_mean_zero line 131
  31. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct_eq_zero_iff line 134
  32. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.mean_add line 137
  33. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.mean_smul line 141
  34. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.mean_mean line 145
  35. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct_add line 149
  36. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct_smul line 153
  37. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fluct_fluct line 156