OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneFluid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The whole-plane scalar produces an actual Navier–Stokes velocity. The force is prescribed from the drift and source, before solving for w.

  1. theorem OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution.hasDerivWithinAt line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution.initialTimeDerivative line 27
  3. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_plane_equation line 43
  4. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_plane_divergence line 59
  5. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_plane_initial line 72
  6. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_third line 79
  7. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_halfPlane_integral line 85

    Source documentation

    Normalized integration over the period-one coordinate gives exactly the scalar half-plane observation used in the construction.

    theorem triangularVelocity_halfPlane_integral (a : ℝ → Plane → Plane)
    (w : ℝ → Plane → ℝ) (t : ℝ) :
    (∫ X in ExpandingDetector.upperHalfPlane, ∫ z in Icc (0 : ℝ) 1,
      triangularVelocity a w (t, atHeight X z) 2) =
      ∫ X in ExpandingDetector.upperHalfPlane, w t X := by
…

    Mentions: OAI.ForcedComputation.ExpandingDetector.upperHalfPlane, OAI.ForcedComputation.VelocityDetector.triangularVelocity