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

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Effective bounds for every mixed derivative of the compact planar processor, with phase represented by the third coordinate.

  1. def OAI.ForcedComputation.planeProjection line 14
  2. theorem OAI.ForcedComputation.planeProjection_apply line 17
  3. def OAI.ForcedComputation.planarMixed line 21
  4. theorem OAI.ForcedComputation.planarMixed_eventuallyEq line 25
  5. theorem OAI.ForcedComputation.planarMixed_zero line 34
  6. theorem OAI.ForcedComputation.planeProjection_mixed line 42
  7. def OAI.ForcedComputation.planarField line 64
  8. theorem OAI.ForcedComputation.planarField_slice line 68
  9. def OAI.ForcedComputation.planarMixedBound line 79
  10. theorem OAI.ForcedComputation.planarMixed_slice_bound line 82
  11. theorem OAI.ForcedComputation.Recorder.Planar.compactPlanarField_germ line 92
  12. theorem OAI.ForcedComputation.Recorder.Planar.compactPlanarField_zero_germ line 105
  13. theorem OAI.ForcedComputation.Recorder.Planar.compactPlanar_mixed_bound line 119