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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The injection is captured before the first moving stage. Testing the actual scalar equation gives the initial mass minus its diffusion loss.

  1. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_mul_unitImpulse line 16
  2. theorem OAI.ForcedComputation.ExpandingDetector.initial_concentration_capture line 31