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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-time strong regularity of the actual expanding drift. A finite prefix agrees on an open time neighborhood, including at the endpoints.

  1. theorem OAI.ForcedComputation.ExpandingDetector.expandingDrift_eq_finite_near line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.expandingDrift_component_regularity line 27