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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The L2 condition removes the spatially constant pressure ambiguity on the infinite cylinder.

  1. theorem OAI.ForcedComputation.VelocityDetector.cylinderMeasure_univ line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.cylinder_classical_pressure_unique line 19
  3. theorem OAI.ForcedComputation.VelocityDetector.cylinder_classical_unique line 56