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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

On the support chart, differentiation commutes exactly with periodization. Consequently every mixed rapid estimate transfers with the same constant.

  1. theorem OAI.RapidForcing.CompactEmbedding.chart_closed line 13
  2. def OAI.RapidForcing.CompactEmbedding.ChartSupported line 22
  3. theorem OAI.RapidForcing.CompactEmbedding.ChartSupported.tsupport line 29
  4. theorem OAI.RapidForcing.CompactEmbedding.ChartSupported.spatialD line 35
  5. theorem OAI.RapidForcing.CompactEmbedding.ChartSupported.timeD line 42
  6. theorem OAI.RapidForcing.CompactEmbedding.ChartSupported.spatialIter line 48
  7. theorem OAI.RapidForcing.CompactEmbedding.ChartSupported.timeIter line 54
  8. theorem OAI.RapidForcing.CompactEmbedding.ChartSupported.mixedD line 60
  9. theorem OAI.RapidForcing.CompactEmbedding.periodic_spatialD line 69
  10. theorem OAI.RapidForcing.CompactEmbedding.periodic_timeD line 90
  11. theorem OAI.RapidForcing.CompactEmbedding.periodic_spatialIter line 92
  12. theorem OAI.RapidForcing.CompactEmbedding.periodic_timeIter line 100
  13. theorem OAI.RapidForcing.CompactEmbedding.periodic_mixedD line 106
  14. theorem OAI.RapidForcing.CompactEmbedding.periodic_mixed_bound line 113
  15. theorem OAI.RapidForcing.CompactEmbedding.periodic_rapid line 120