feat(FluidDynamics): Adding more fluid dynamics - continuation of PR #949 and #1112 ,

Physlib.lean

@@ -60,10 +60,14 @@ 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.Basic
+public import Physlib.FluidDynamics.CauchyMomentum
+public import Physlib.FluidDynamics.Continuity
+public import Physlib.FluidDynamics.Euler.Basic
+public import Physlib.FluidDynamics.Euler.Bernoulli
+public import Physlib.FluidDynamics.Incompressible
+public import Physlib.FluidDynamics.Momentum
 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

Physlib/FluidDynamics/Basic.lean

@@ -0,0 +1,178 @@
+/-
+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.Derivatives.Grad
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+
+# Fluid flows
+
+## i. Overview
+
+This module defines the basic fields used to describe a fluid on `d`-dimensional space.
+The core structure `FluidFlow` contains only the density and velocity fields, so it is the
+minimal data needed for kinematic and mass-transport constructions such as continuity,
+incompressibility, momentum density, and material derivatives. The structure `CauchyFlow`
+adds Cauchy stress and specific body-force fields, the extra data used for momentum balances.
+The structure `ThermodynamicCauchyFlow` adds entropy and enthalpy fields for thermodynamic
+laws such as Bernoulli-type statements.
+
+## 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.
+- `FluidFlow` : The density and velocity fields of a fluid.
+- `CauchyFlow` : A fluid flow with Cauchy stress and specific body force.
+- `ThermodynamicCauchyFlow` : A Cauchy flow with entropy and enthalpy fields.
+- `FluidFlow.DensityTimeIndependent` : A fluid flow whose density has zero time derivative.
+- `FluidFlow.VelocityTimeIndependent` : A fluid flow whose velocity has zero time derivative.
+- `FluidFlow.materialDerivative` : The material derivative along a fluid velocity field.
+- `FluidFlow.specificKineticEnergy` : The specific kinetic energy `|u|^2 / 2`.
+- `ThermodynamicCauchyFlow.IsIsentropic` : A thermodynamic Cauchy flow whose entropy is
+  materially conserved.
+
+## iii. Table of contents
+
+- A. Field types
+- B. Fluid flow structures
+- C. Time-independence predicates
+- D. Flow-derived scalar quantities
+- E. Thermodynamic-flow predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open scoped InnerProductSpace
+open Space
+open Time
+
+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) ℝ
+
+/-!
+
+## B. Fluid flow structures
+
+-/
+
+/-- The density and velocity fields of a fluid on `d`-dimensional space.
+
+This is the kinematic/mass-transport layer of the fluid API. It intentionally contains no
+stress, body force, or thermodynamic fields. Those are introduced only by the extension
+structures that need them. -/
+structure FluidFlow (d : ℕ) where
+  /-- The mass density field. -/
+  rho : MassDensity d
+  /-- The velocity field. -/
+  velocity : VelocityField d
+
+/-- A fluid flow equipped with Cauchy stress and specific body-force fields.
+
+This is the momentum-balance layer of the fluid API. The Cauchy stress is the primitive
+dynamic field; pressure and viscosity enter through stress laws rather than as fields of
+`CauchyFlow` itself. -/
+structure CauchyFlow (d : ℕ) extends FluidFlow d where
+  /-- The Cauchy stress tensor field. -/
+  stress : StressTensor d
+  /-- The specific body-force field, i.e. force per unit mass. -/
+  specificBodyForce : VectorField d
+
+/-- A Cauchy flow equipped with thermodynamic entropy and enthalpy fields.
+
+This extends the kinematic and momentum-balance data with thermodynamic fields used by
+isentropic and Bernoulli-type laws. -/
+structure ThermodynamicCauchyFlow (d : ℕ) extends CauchyFlow d where
+  /-- The specific entropy field. -/
+  entropy : ScalarField d
+  /-- The specific enthalpy field. -/
+  enthalpy : ScalarField d
+
+/-!
+
+## C. Time-independence predicates
+
+-/
+
+namespace FluidFlow
+
+/-- A fluid flow has time-independent density when the density has zero time derivative at
+each spatial point. -/
+def DensityTimeIndependent (d : ℕ) (fluid : FluidFlow d) : Prop :=
+  ∀ t x, ∂ₜ (fluid.rho · x) t = 0
+
+/-- A fluid flow has time-independent velocity when the velocity has zero time derivative at
+each spatial point. -/
+def VelocityTimeIndependent (d : ℕ) (fluid : FluidFlow d) : Prop :=
+  ∀ t x, ∂ₜ (fluid.velocity · x) t = 0
+
+end FluidFlow
+
+/-!
+
+## D. Flow-derived scalar quantities
+
+-/
+
+namespace FluidFlow
+
+/-- The material derivative `D_t f = partial_t f + u · grad f` of a scalar field. -/
+noncomputable def materialDerivative (d : ℕ) (fluid : FluidFlow d)
+    (field : ScalarField d) : ScalarField d :=
+  fun t x => ∂ₜ (field · x) t + ⟪fluid.velocity t x, ∇ (field t) x⟫_ℝ
+
+/-- The specific kinetic energy `|u|^2 / 2` of a fluid flow. -/
+noncomputable def specificKineticEnergy (d : ℕ) (fluid : FluidFlow d) : ScalarField d :=
+  fun t x => (1 / 2 : ℝ) * ⟪fluid.velocity t x, fluid.velocity t x⟫_ℝ
+
+end FluidFlow
+
+/-!
+
+## E. Thermodynamic-flow predicates
+
+-/
+
+namespace ThermodynamicCauchyFlow
+
+/-- A thermodynamic flow is isentropic when the entropy is materially conserved along the
+underlying fluid velocity field. -/
+def IsIsentropic (d : ℕ) (flow : ThermodynamicCauchyFlow d) : Prop :=
+  ∀ t x, FluidFlow.materialDerivative d flow.toFluidFlow flow.entropy t x = 0
+
+end ThermodynamicCauchyFlow
+
+end FluidDynamics

Physlib/FluidDynamics/CauchyMomentum.lean

@@ -0,0 +1,139 @@
+/-
+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.Momentum
+/-!
+
+# Cauchy momentum equations
+
+## i. Overview
+
+This module defines the conservative and convective Cauchy momentum equations for a fluid flow
+with stress and specific body-force fields. The stress tensor is left as an input field, so this
+is the balance-law layer before specializing to a constitutive law, such as Euler or
+Navier-Stokes.
+
+## ii. Key results
+
+- `CauchyFlow.CauchyMomentumEquation` : Conservation of momentum using `Space.matrixDiv`.
+- `CauchyFlow.ConvectiveCauchyMomentumEquation` : The Cauchy momentum equation in convective
+  form.
+- `CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation` : Equivalence of the
+  two Cauchy momentum equations when continuity holds and the fields are differentiable.
+
+## iii. Table of contents
+
+- A. Cauchy momentum equations
+- B. Equivalence of conservative and convective Cauchy momentum
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+namespace CauchyFlow
+
+/-!
+
+## A. Cauchy momentum equations
+
+-/
+
+/-- Conservation of momentum in conservative matrix-divergence form.
+
+The equation is
+
+`partial_t (rho u) + matrixDiv (rho u ⊗ u) = matrixDiv sigma + rho f`.
+
+Here `stress` is intentionally not yet specialized to a constitutive law.
+-/
+def CauchyMomentumEquation (d : ℕ) (flow : CauchyFlow d) : Prop :=
+  ∀ t x,
+    FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+
+/-- Conservation of momentum in convective form.
+
+The equation is
+
+`rho (partial_t u + (u · ∇)u) = matrixDiv sigma + rho f`.
+
+Here `stress` is intentionally not yet specialized to a constitutive law.
+-/
+def ConvectiveCauchyMomentumEquation (d : ℕ) (flow : CauchyFlow d) : Prop :=
+  ∀ t x,
+    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+
+/-!
+
+## B. Equivalence of conservative and convective Cauchy momentum
+
+-/
+
+/-- The conservative and convective Cauchy momentum equations are equivalent when the classical
+continuity equation holds.
+
+The differentiability assumptions are exactly the product-rule assumptions used to rewrite
+`partial_t (rho u)` and `matrixDiv (rho u ⊗ u)`.
+-/
+theorem cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation
+    (d : ℕ) (flow : CauchyFlow d)
+    (hContinuity : FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow)
+    (hRhoTime : ∀ t x, DifferentiableAt ℝ (flow.rho · x) t)
+    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (flow.velocity · x) t)
+    (hMomentumDensity : ∀ t, Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (flow.velocity t)) :
+    CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow := by
+  constructor
+  · intro hConservative t x
+    have hMassFluxSpace :
+        DifferentiableAt ℝ (fun x' => flow.rho t x' • flow.velocity t x') x := by
+      simpa [FluidFlow.momentumDensity] using (hMomentumDensity t).differentiableAt
+    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := by
+      simpa [FluidFlow.continuityResidual] using
+        hContinuity t x (by simpa using hRhoTime t x) hMassFluxSpace
+    have hLhs :=
+      FluidFlow.conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t)
+    have hLhs' :
+        FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+          FluidFlow.convectiveMomentumLHS d flow.toFluidFlow t x := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change FluidFlow.convectiveMomentumLHS d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+    rw [← hLhs']
+    exact hConservative t x
+  · intro hConvective t x
+    have hMassFluxSpace :
+        DifferentiableAt ℝ (fun x' => flow.rho t x' • flow.velocity t x') x := by
+      simpa [FluidFlow.momentumDensity] using (hMomentumDensity t).differentiableAt
+    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := by
+      simpa [FluidFlow.continuityResidual] using
+        hContinuity t x (by simpa using hRhoTime t x) hMassFluxSpace
+    have hLhs :=
+      FluidFlow.conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t)
+    have hLhs' :
+        FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+          FluidFlow.convectiveMomentumLHS d flow.toFluidFlow t x := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+    rw [hLhs']
+    exact hConvective t x
+
+end CauchyFlow
+
+end FluidDynamics