OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingForceSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual Navier–Stokes force has compact horizontal support on each finite time interval, including all time derivatives of the prescribed drift.

  1. def OAI.ForcedComputation.ExpandingDetector.finiteDrift line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.finiteDrift_smooth line 19
  3. theorem OAI.ForcedComputation.ExpandingDetector.finiteDrift_compact_family line 27
  4. theorem OAI.ForcedComputation.ExpandingDetector.expandingForce_compact_on_finite_intervals line 46