feat(FluidDynamics): add Navier-Stokes conservative and convective forms

Physlib.lean

@@ -50,6 +50,10 @@ public import Physlib.Electromagnetism.ThreeDimension.MaxwellEquations
 public import Physlib.Electromagnetism.Vacuum.Constant
 public import Physlib.Electromagnetism.Vacuum.HarmonicWave
 public import Physlib.Electromagnetism.Vacuum.IsPlaneWave
+public import Physlib.FluidDynamics.FluidState
+public import Physlib.FluidDynamics.NavierStokes.Basic
+public import Physlib.FluidDynamics.NavierStokes.Continuity
+public import Physlib.FluidDynamics.NavierStokes.Momentum
 public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
@@ -360,6 +364,7 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Div
 public import Physlib.SpaceAndTime.Space.Derivatives.Grad
 public import Physlib.SpaceAndTime.Space.Derivatives.Iterated
 public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian
+public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv
 public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
 public import Physlib.SpaceAndTime.Space.DistConst
 public import Physlib.SpaceAndTime.Space.DistOfFunction

Physlib/FluidDynamics/FluidState.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner
+-/
+module
+
+public import Physlib.SpaceAndTime.Space.Basic
+public import Physlib.SpaceAndTime.Time.Basic
+/-!
+
+# Fluid states
+
+## i. Overview
+
+This module defines the basic fields used to describe a fluid on `d`-dimensional space.
+The core structure `FluidState` contains only the density and velocity fields. Additional
+fields used by specific balance laws are provided by extension structures.
+
+## ii. Key results
+
+- `ScalarField` : A time-dependent scalar field on space.
+- `VectorField` : A time-dependent vector field on space.
+- `MassDensity` : A time-dependent scalar density field.
+- `VelocityField` : A time-dependent vector velocity field.
+- `MomentumDensityField` : A time-dependent vector momentum density field.
+- `StressTensor` : A time-dependent matrix-valued stress field.
+- `BodyForce` : A time-dependent vector body-force field per unit mass.
+- `FluidState` : The density and velocity fields of a fluid.
+- `FluidInMomentumBalance` : A fluid state with stress and body force.
+
+## iii. Table of contents
+
+- A. Field types
+- B. Fluid state structures
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Field types
+
+-/
+
+/-- A scalar field on `d`-dimensional space, depending on time. -/
+abbrev ScalarField (d : ℕ) := Time → Space d → ℝ
+
+/-- A vector field on `d`-dimensional space, depending on time. -/
+abbrev VectorField (d : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin d)
+
+/-- A mass density field on `d`-dimensional space. -/
+abbrev MassDensity (d : ℕ) := ScalarField d
+
+/-- A velocity field on `d`-dimensional space. -/
+abbrev VelocityField (d : ℕ) := VectorField d
+
+/-- A momentum density field on `d`-dimensional space. -/
+abbrev MomentumDensityField (d : ℕ) := VectorField d
+
+/-- A matrix-valued stress tensor field on `d`-dimensional space. -/
+abbrev StressTensor (d : ℕ) := Time → Space d → Matrix (Fin d) (Fin d) ℝ
+
+/-- A body-force field per unit mass on `d`-dimensional space. -/
+abbrev BodyForce (d : ℕ) := VectorField d
+
+/-!
+
+## B. Fluid state structures
+
+-/
+
+/-- The density and velocity fields of a fluid on `d`-dimensional space. -/
+structure FluidState (d : ℕ) where
+  /-- The mass density field. -/
+  rho : MassDensity d
+  /-- The velocity field. -/
+  velocity : VelocityField d
+
+/-- The fields needed for a momentum balance: fluid state, stress, and body force. -/
+structure FluidInMomentumBalance (d : ℕ) extends FluidState d where
+  /-- The stress tensor field. -/
+  stress : StressTensor d
+  /-- The body-force field per unit mass. -/
+  bodyForce : BodyForce d
+
+end FluidDynamics

Physlib/FluidDynamics/NavierStokes/Basic.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner
+-/
+module
+
+public import Physlib.FluidDynamics.NavierStokes.Momentum
+/-!
+
+# The Navier-Stokes equations
+
+## i. Overview
+
+The Navier-Stokes equations are a set of partial differential equations that describe
+the motion of viscous fluid substances. They are fundamental in fluid dynamics and are
+used to model the behavior of fluids in various contexts, including gas flow and water flow.
+
+This file combines the classical continuity equation with the momentum equation. The stress
+tensor is left as an input field, so this is the balance-law layer before specializing to a
+Newtonian stress law.
+
+## ii. Key results
+
+- `NavierStokes` : Classical continuity and conservative momentum equations together.
+- `ConvectiveNavierStokes` : Classical continuity and convective momentum equations together.
+- `NavierStokes_iff_ConvectiveNavierStokes` : Equivalence of the two forms when the
+  fields are differentiable.
+
+## iii. Table of contents
+
+- A. Full Navier-Stokes forms
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Full Navier-Stokes forms
+
+-/
+
+/-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
+def NavierStokes (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
+  FluidDynamics.NavierStokes.ClassicalContinuityEquation d data.toFluidState ∧
+    FluidDynamics.NavierStokes.MomentumEquation d data
+
+/-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
+def ConvectiveNavierStokes (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
+  FluidDynamics.NavierStokes.ClassicalContinuityEquation d data.toFluidState ∧
+    FluidDynamics.NavierStokes.ConvectiveMomentumEquation d data
+
+/-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
+differentiable enough for the product rules. -/
+theorem navierStokes_iff_convectiveNavierStokes
+    (d : ℕ) (data : FluidInMomentumBalance d)
+    (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)
+    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (data.velocity · x) t)
+    (hMomentumDensity : ∀ t,
+      Differentiable ℝ (FluidDynamics.NavierStokes.momentumDensity d data.toFluidState t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
+    NavierStokes d data ↔ ConvectiveNavierStokes d data := by
+  constructor
+  · intro hConservative
+    refine ⟨hConservative.1, ?_⟩
+    exact (FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data
+      hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp hConservative.2
+  · intro hConvective
+    refine ⟨hConvective.1, ?_⟩
+    exact (FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data
+      hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr hConvective.2
+
+end FluidDynamics

Physlib/FluidDynamics/NavierStokes/Continuity.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner
+-/
+module
+
+public import Physlib.FluidDynamics.FluidState
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+
+# The Navier-Stokes continuity equation
+
+## i. Overview
+
+This module defines the classical conservative mass-balance equation for a fluid state and
+the corresponding continuity residual.
+
+## ii. Key results
+
+- `ClassicalContinuityEquation` : Classical conservation of mass in conservative form.
+- `continuityResidual` : The scalar residual `partial_t rho + div (rho u)`.
+- `SmoothContinuityEquation` : Continuity for globally differentiable fields.
+- `SmoothContinuityEquation.toClassical` : Smooth continuity implies classical continuity.
+
+## iii. Table of contents
+
+- A. Continuity equations
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+namespace NavierStokes
+
+/-!
+
+## A. Continuity equations
+
+-/
+
+/-- Classical conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`.
+
+The equation is asserted at points where the time derivative of `rho` and the spatial
+divergence of `rho u` are classical derivatives.
+-/
+def ClassicalContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
+  ∀ t x, DifferentiableAt ℝ (fluid.rho · x) t →
+      DifferentiableAt ℝ (fun x' => fluid.rho t x' • fluid.velocity t x') x →
+        ∂ₜ (fluid.rho · x) t + (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x = 0
+
+/-- The scalar continuity-equation residual
+`partial_t rho + div (rho u)`. -/
+noncomputable def continuityResidual (d : ℕ) (fluid : FluidState d) : Time → Space d → ℝ :=
+  fun t x => ∂ₜ (fluid.rho · x) t + (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x
+
+/-- A stronger continuity equation for globally differentiable fields.
+
+This version records the first-order regularity needed by the classical continuity equation:
+the density is differentiable in time, the mass flux `rho u` is differentiable in space, and
+the continuity residual vanishes everywhere.
+-/
+def SmoothContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
+  (∀ x, Differentiable ℝ (fluid.rho · x)) ∧
+    (∀ t, Differentiable ℝ (fun x => fluid.rho t x • fluid.velocity t x)) ∧
+      ∀ t x, continuityResidual d fluid t x = 0
+
+/-- A smooth continuity equation satisfies the guarded classical continuity equation. -/
+lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidState d) :
+    SmoothContinuityEquation d fluid → ClassicalContinuityEquation d fluid := by
+  intro hSmooth t x _ _
+  simpa [continuityResidual] using hSmooth.2.2 t x
+
+end NavierStokes
+end FluidDynamics