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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The detector's actual scalar has the small total mass of the injected bumps. Incompressible stirring and diffusion make no contribution.

  1. def OAI.ForcedComputation.VelocityDetector.detectorPartialMass line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorPartialMass_continuous line 19
  3. theorem OAI.ForcedComputation.VelocityDetector.detectorPartialMass_hasDerivAt line 25
  4. theorem OAI.ForcedComputation.VelocityDetector.detectorPartialMass_zero line 36
  5. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_mass line 46
  6. theorem OAI.ForcedComputation.VelocityDetector.detectorPartialMass_bound line 66
  7. theorem OAI.ForcedComputation.VelocityDetector.detector_scalar_mass_bound line 81