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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One scalar construction gives the halting observation and unique classical fluid at every positive viscosity. The force is prescribed from the processor and source, before the scalar solution is chosen.

  1. theorem OAI.ForcedComputation.VelocityDetector.processor_detector_all_viscosities line 18