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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Time collars, incompressibility and rigid motion for the entire finite recorder array. The array includes every defined address transition.

  1. theorem OAI.ForcedComputation.ExpandingDetector.recorderStageField_zero_before line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.recorderStageField_zero_after line 23
  3. theorem OAI.ForcedComputation.ExpandingDetector.recorderStageField_properties line 32
  4. theorem OAI.ForcedComputation.ExpandingDetector.recorderStageField_rigid line 42