OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/CompactPeriodization.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Periodization in a chart strictly separated from every integer face. The fractional representative is only a definition: smoothness follows from local translation or local zero, so no differentiability of the fractional part at an integer is asserted.

  1. def OAI.RapidForcing.CompactEmbedding.latticeVector line 15
  2. def OAI.RapidForcing.CompactEmbedding.representative line 17
  3. theorem OAI.RapidForcing.CompactEmbedding.representative_apply line 19
  4. theorem OAI.RapidForcing.CompactEmbedding.latticeVector_apply line 22
  5. theorem OAI.RapidForcing.CompactEmbedding.representative_add_lattice line 25
  6. theorem OAI.RapidForcing.CompactEmbedding.representative_eq line 30
  7. def OAI.RapidForcing.CompactEmbedding.periodic line 35
  8. theorem OAI.RapidForcing.CompactEmbedding.periodic_add_lattice line 37
  9. theorem OAI.RapidForcing.CompactEmbedding.periodic_eq_on_chart line 42
  10. theorem OAI.RapidForcing.CompactEmbedding.representative_local_translation line 48
  11. theorem OAI.RapidForcing.CompactEmbedding.fract_near_integer line 62
  12. theorem OAI.RapidForcing.CompactEmbedding.representative_local_outside line 78
  13. theorem OAI.RapidForcing.CompactEmbedding.periodic_local line 89
  14. theorem OAI.RapidForcing.CompactEmbedding.periodic_smooth line 104