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.CauchyMomentum
+public import Physlib.FluidDynamics.Continuity
+public import Physlib.FluidDynamics.Euler.Basic
+public import Physlib.FluidDynamics.Euler.Bernoulli
+public import Physlib.FluidDynamics.FluidFlow
+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/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.cauchy_momentum_iff_convective_cauchy_momentum` : 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 cauchy_momentum_iff_convective_cauchy_momentum
+    (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

Physlib/FluidDynamics/NavierStokes/Continuity.lean → Physlib/FluidDynamics/Continuity.lean

@@ -5,24 +5,26 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Physlib.FluidDynamics.FluidState
+public import Physlib.FluidDynamics.FluidFlow
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 public import Physlib.SpaceAndTime.Time.Derivatives
 /-!
 
-# The Navier-Stokes continuity equation
+# Continuity equation for fluid flows
 
 ## i. Overview
 
-This module defines the classical conservative mass-balance equation for a fluid state and
-the corresponding continuity residual.
+This module defines the classical conservative mass-balance equation for a fluid flow and the
+corresponding continuity residual. These definitions are independent of a particular momentum
+equation, so they can be reused by Navier-Stokes, Euler, and other fluid models.
 
 ## 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.
+- `FluidFlow.ClassicalContinuityEquation` : Classical conservation of mass in conservative form.
+- `FluidFlow.continuityResidual` : The scalar residual `partial_t rho + div (rho u)`.
+- `FluidFlow.SmoothContinuityEquation` : Continuity for globally differentiable fields.
+- `FluidFlow.SmoothContinuityEquation.toClassical` : Smooth continuity implies classical
+  continuity.
 
 ## iii. Table of contents
 
@@ -38,7 +40,8 @@ open Space
 open Time
 
 namespace FluidDynamics
-namespace NavierStokes
+
+namespace FluidFlow
 
 /-!
 
@@ -51,14 +54,14 @@ namespace NavierStokes
 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 :=
+def ClassicalContinuityEquation (d : ℕ) (fluid : FluidFlow 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 → ℝ :=
+noncomputable def continuityResidual (d : ℕ) (fluid : FluidFlow 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.
@@ -67,16 +70,17 @@ This version records the first-order regularity needed by the classical continui
 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 :=
+def SmoothContinuityEquation (d : ℕ) (fluid : FluidFlow 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) :
+lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidFlow d) :
     SmoothContinuityEquation d fluid → ClassicalContinuityEquation d fluid := by
   intro hSmooth t x _ _
   simpa [continuityResidual] using hSmooth.2.2 t x
 
-end NavierStokes
+end FluidFlow
+
 end FluidDynamics

Physlib/FluidDynamics/Euler/Basic.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner, Michał Mogielnicki
+-/
+module
+
+public import Physlib.FluidDynamics.CauchyMomentum
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+/-!
+
+# Euler equation for fluid flows
+
+## i. Overview
+
+This module defines the Euler equations for inviscid fluid flow as continuity, Cauchy momentum,
+and an inviscid stress law. The pressure field appears through the constitutive relation for
+the Cauchy stress tensor rather than as a field of the flow data.
+
+## ii. Key results
+
+- `CauchyFlow.IsInviscid` : Predicate saying the Cauchy stress is the inviscid pressure stress.
+- `CauchyFlow.matrixDiv_stress_eq_neg_grad_pressure_of_is_inviscid` : The inviscid stress
+  contributes the usual pressure-gradient force term.
+- `Euler` : Classical continuity, Cauchy momentum, and inviscid stress together.
+- `ConvectiveEuler` : Classical continuity, convective Cauchy momentum, and inviscid stress.
+- `euler_iff_convective_euler` : Equivalence of the conservative and convective forms when the
+  fields are differentiable.
+
+## iii. Table of contents
+
+- A. Inviscid stress law
+- B. Euler equations
+- C. Equivalence of conservative and convective Euler forms
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+namespace CauchyFlow
+
+/-!
+
+## A. Inviscid stress law
+
+-/
+
+/-- A Cauchy flow is inviscid with pressure `p` when its stress is `-p I`. -/
+def IsInviscid (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
+  ∀ t x, flow.stress t x = (-(pressure t x)) • (1 : Matrix (Fin d) (Fin d) ℝ)
+
+/-- The matrix divergence of the inviscid pressure stress `-p I` is `-grad p`. -/
+lemma matrixDiv_inviscid_pressure_stress (d : ℕ) (pressureAtTime : Space d → ℝ) :
+    matrixDiv d (fun x => (-(pressureAtTime x)) • (1 : Matrix (Fin d) (Fin d) ℝ)) =
+      -∇ pressureAtTime := by
+  ext x i
+  rw [matrixDiv_apply]
+  rw [Finset.sum_eq_single i]
+  · simp [grad, Space.deriv_eq]
+  · intro j _ hji
+    have hij : i ≠ j := fun h => hji h.symm
+    simp [hij]
+  · intro hi
+    simp at hi
+
+/-- In an inviscid Cauchy flow, the stress-divergence force is the usual
+negative pressure-gradient term. -/
+theorem matrixDiv_stress_eq_neg_grad_pressure_of_is_inviscid
+    (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d)
+    (hInviscid : IsInviscid d flow pressure) :
+    ∀ t, matrixDiv d (flow.stress t) = -∇ (pressure t) := by
+  intro t
+  rw [show flow.stress t =
+      fun x => (-(pressure t x)) • (1 : Matrix (Fin d) (Fin d) ℝ) by
+    funext x
+    exact hInviscid t x]
+  exact matrixDiv_inviscid_pressure_stress d (pressure t)
+
+end CauchyFlow
+
+/-!
+
+## B. Euler equations
+
+-/
+
+/-- The conservative Euler equations: continuity, Cauchy momentum, and inviscid stress. -/
+def Euler (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
+  FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow ∧
+    CauchyFlow.CauchyMomentumEquation d flow ∧ CauchyFlow.IsInviscid d flow pressure
+
+/-- The convective Euler equations: continuity, convective Cauchy momentum, and inviscid
+stress. -/
+def ConvectiveEuler (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
+  FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow ∧
+    CauchyFlow.ConvectiveCauchyMomentumEquation d flow ∧ CauchyFlow.IsInviscid d flow pressure
+
+/-!
+
+## C. Equivalence of conservative and convective Euler forms
+
+-/
+
+/-- The conservative and convective Euler forms are equivalent when the fields are
+differentiable enough for the product rules. -/
+theorem euler_iff_convective_euler
+    (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d)
+    (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)) :
+    Euler d flow pressure ↔ ConvectiveEuler d flow pressure := by
+  constructor
+  · intro hConservative
+    refine ⟨hConservative.1, ?_, hConservative.2.2⟩
+    exact (CauchyFlow.cauchy_momentum_iff_convective_cauchy_momentum d flow hConservative.1
+      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp hConservative.2.1
+  · intro hConvective
+    refine ⟨hConvective.1, ?_, hConvective.2.2⟩
+    exact (CauchyFlow.cauchy_momentum_iff_convective_cauchy_momentum d flow hConvective.1
+      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr hConvective.2.1
+
+end FluidDynamics