OAI/MathematicalPhysics/RecorderFlows/Model.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Periodic incompressible fields, classical solutions and bounded smooth forcing.

  1. abbrev OAI.Solenoidal.Fluid.Space line 11
  2. abbrev OAI.Solenoidal.Fluid.SpaceTime line 12
  3. abbrev OAI.Solenoidal.Fluid.Field line 13
  4. abbrev OAI.Solenoidal.Fluid.Pressure line 14
  5. def OAI.Solenoidal.Fluid.point line 16
  6. def OAI.Solenoidal.Fluid.translateTime line 18
  7. def OAI.Solenoidal.Fluid.translateSpace line 21
  8. def OAI.Solenoidal.Fluid.SpatiallyPeriodic line 24
  9. def OAI.Solenoidal.Fluid.partialD line 27
  10. def OAI.Solenoidal.Fluid.mixedD line 30
  11. def OAI.Solenoidal.Fluid.diverge line 34
  12. def OAI.Solenoidal.Fluid.laplacian line 37
  13. def OAI.Solenoidal.Fluid.advection line 40
  14. def OAI.Solenoidal.Fluid.force line 44
  15. def OAI.Solenoidal.Fluid.cell line 48
  16. def OAI.Solenoidal.Fluid.spatialMean line 50
  17. def OAI.Solenoidal.Fluid.pressureMean line 53
  18. def OAI.Solenoidal.Fluid.energy line 56
  19. def OAI.Solenoidal.Fluid.BoundedMixed line 60
  20. def OAI.Solenoidal.Fluid.PeriodicAfterOne line 64
  21. def OAI.Solenoidal.Fluid.ZeroNearIntegers line 67
  22. structure OAI.Solenoidal.Fluid.ClassicalSolutionOn line 73
  23. def OAI.Solenoidal.Fluid.FluidAssertions line 113
  24. def OAI.Solenoidal.Fluid.BoundedPeriodicAssertions line 124