OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicFamilyAlgebra.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Algebra and support preservation for periodic families on an open domain.

  1. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.inner_add_left line 14
  2. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.inner_add_right line 17
  3. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.angle_zero_at line 21
  4. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.slow_zero_on line 30
  5. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.vectorMean line 41
  6. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.vectorMean_apply line 44
  7. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.centered_mean_zero line 52
  8. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.primitive_zero_at line 58
  9. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.primitive_mem line 66
  10. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.mean line 84
  11. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct line 86
  12. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.mean_apply line 88
  13. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct_apply line 90
  14. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct_mean_zero line 94
  15. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.mean_add line 99
  16. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.mean_smul line 103
  17. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.mean_mean line 107
  18. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct_add line 113
  19. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct_smul line 116
  20. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct_fluct line 118
  21. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.fluct_zero_at line 123