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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The analytic detector assembly. Published scalar existence and heat inputs are explicit, as are the smooth-dependence inputs for the given planar flow. The quantitative comparison and observation are proved here.

  1. theorem OAI.ForcedComputation.VelocityDetector.detector_observation line 16