OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/UniformForceBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Every mixed derivative of the actual whole-plane force is bounded for all time. The source and the complete drift are prescribed first.

  1. theorem OAI.ForcedComputation.VelocityDetector.UniformJets.mixed line 16
  2. theorem OAI.ForcedComputation.VelocityDetector.UniformJets.mixed_bound line 22
  3. theorem OAI.ForcedComputation.VelocityDetector.UniformJets.force line 28
  4. theorem OAI.ForcedComputation.VelocityDetector.UniformJets.convection line 42
  5. theorem OAI.ForcedComputation.VelocityDetector.UniformJets.residual line 55
  6. def OAI.ForcedComputation.VelocityDetector.horizontalTimeProjection line 60
  7. theorem OAI.ForcedComputation.VelocityDetector.unitImpulse_compactSupport line 64
  8. theorem OAI.ForcedComputation.VelocityDetector.expandingForce_all_mixed_bounded line 82