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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The explicit detector source and drift have one global smooth, nonnegative scalar evolution, conditional only on the published existence input. The drift and source never depend on this unknown scalar.

  1. theorem OAI.ForcedComputation.VelocityDetector.detectorScalar_exists line 15