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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar computation detector is a full classical Navier–Stokes solution, unique in the cylinder comparison class.

  1. def OAI.ForcedComputation.ExpandingDetector.upperCylinderMass line 17

    Source documentation

    The observed mass integrates over the entire unit vertical period.

    def upperCylinderMass (u : Velocity) (t : ℝ) : ℝ :=
…
  2. theorem OAI.ForcedComputation.ExpandingDetector.upperCylinderMass_triangular line 20
  3. def OAI.ForcedComputation.ExpandingDetector.WholePlaneDetection line 26
  4. theorem OAI.ForcedComputation.ExpandingDetector.expanding_fluid_detection line 38