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

Physlib.lean

@@ -60,9 +60,13 @@ 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.Continuity
+public import Physlib.FluidDynamics.Euler.Basic
+public import Physlib.FluidDynamics.Euler.Bernoulli
 public import Physlib.FluidDynamics.FluidState
+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

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

@@ -10,12 +10,13 @@ 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 state 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
 
@@ -38,7 +39,6 @@ open Space
 open Time
 
 namespace FluidDynamics
-namespace NavierStokes
 
 /-!
 
@@ -78,5 +78,4 @@ lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidState d) :
   intro hSmooth t x _ _
   simpa [continuityResidual] using hSmooth.2.2 t x
 
-end NavierStokes
 end FluidDynamics

Physlib/FluidDynamics/Euler/Basic.lean

@@ -0,0 +1,138 @@
+/-
+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.Momentum
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+/-!
+
+# Euler equation for fluid flows
+
+## i. Overview
+
+This module defines the Euler momentum equation for inviscid fluid flow. The pressure gradient
+and body force terms are kept explicit, while the conservative and convective left-hand sides
+reuse the corresponding Navier-Stokes balance-law definitions.
+
+## ii. Key results
+
+- `FluidInEulerBalance` : A fluid state with pressure and body force.
+- `eulerForceDensity` : The pressure-gradient and body-force density in Euler momentum balance.
+- `Euler` : Classical continuity and conservative Euler momentum together.
+- `euler_iff_convective_euler` : Equivalence of the conservative and convective forms when the
+  fields are differentiable.
+
+## iii. Table of contents
+
+- A. Euler data
+- B. Euler force density
+- C. Euler equation
+- D. Equivalence of conservative and convective Euler forms
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+
+/-!
+
+## A. Euler data
+
+-/
+
+/-- The fields needed for Euler momentum balance: fluid state, pressure, and body force. -/
+structure FluidInEulerBalance (d : ℕ) extends FluidState d where
+  /-- The pressure field. -/
+  pressure : ScalarField d
+  /-- The body-force field per unit mass. -/
+  bodyForce : BodyForce d
+
+/-!
+
+## B. Euler force density
+
+-/
+
+/-- The force density in Euler momentum balance, `-grad p + rho f`. -/
+noncomputable def eulerForceDensity (d : ℕ) (data : FluidInEulerBalance d) : VectorField d :=
+  fun t x => -(∇ (data.pressure t) x) + data.rho t x • data.bodyForce t x
+
+/-!
+
+## C. Euler equation
+
+-/
+
+/-- The conservative Euler equations: classical continuity and conservative momentum balance. -/
+def Euler (d : ℕ) (data : FluidInEulerBalance d) : Prop :=
+  ClassicalContinuityEquation d data.toFluidState ∧
+    ∀ t x, conservativeMomentumLHS d data.toFluidState t x = eulerForceDensity d data t x
+
+/-!
+
+## D. 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 : ℕ) (data : FluidInEulerBalance d)
+    (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)
+    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (data.velocity · x) t)
+    (hMomentumDensity : ∀ t,
+      Differentiable ℝ (momentumDensity d data.toFluidState t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
+    Euler d data ↔
+      ClassicalContinuityEquation d data.toFluidState ∧
+        ∀ t x, convectiveMomentumLHS d data.toFluidState t x = eulerForceDensity d data t x := by
+  constructor
+  · intro hConservative
+    refine ⟨hConservative.1, ?_⟩
+    intro t x
+    have hMassFluxSpace :
+        DifferentiableAt ℝ (fun x' => data.rho t x' • data.velocity t x') x := by
+      simpa [momentumDensity] using (hMomentumDensity t).differentiableAt
+    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
+      simpa [continuityResidual] using
+        hConservative.1 t x (by simpa using hRhoTime t x) hMassFluxSpace
+    have hLhs :=
+      conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+        d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t)
+    have hLhs' :
+        conservativeMomentumLHS d data.toFluidState t x =
+          convectiveMomentumLHS d data.toFluidState t x := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    rw [← hLhs']
+    exact hConservative.2 t x
+  · intro hConvective
+    refine ⟨hConvective.1, ?_⟩
+    intro t x
+    have hMassFluxSpace :
+        DifferentiableAt ℝ (fun x' => data.rho t x' • data.velocity t x') x := by
+      simpa [momentumDensity] using (hMomentumDensity t).differentiableAt
+    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
+      simpa [continuityResidual] using
+        hConvective.1 t x (by simpa using hRhoTime t x) hMassFluxSpace
+    have hLhs :=
+      conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+        d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t)
+    have hLhs' :
+        conservativeMomentumLHS d data.toFluidState t x =
+          convectiveMomentumLHS d data.toFluidState t x := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    rw [hLhs']
+    exact hConvective.2 t x
+
+end FluidDynamics

Physlib/FluidDynamics/Euler/Bernoulli.lean

@@ -0,0 +1,131 @@
+/-
+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.Euler.Basic
+/-!
+
+# Bernoulli theory for Euler flows
+
+## i. Overview
+
+This module is reserved for Bernoulli definitions and results derived from Euler-flow
+assumptions. The intended development includes the Bernoulli function associated with
+velocity, enthalpy, and an external potential, together with assumptions under which it is
+conserved.
+
+## ii. Key results
+
+- `FluidInBernoulliFlow` : Euler-flow data with enthalpy and potential fields.
+- `HasConservativeBodyForce` : Predicate encoding the convention `bodyForce = -grad Phi`.
+- `IsSteady` : Predicate saying the velocity field has no time dependence.
+- `materialDerivative` : Material derivative of a scalar field along a fluid velocity field.
+- `IsIsentropic` : Predicate saying the entropy is materially conserved.
+- `specificKineticEnergy` : The specific kinetic energy `|u|^2 / 2`.
+- `bernoulliFunction` : The Bernoulli function `|u|^2 / 2 + h + Phi`.
+- `LocalBernoulliLaw` : Vanishing spatial gradient of the Bernoulli function.
+- `BernoulliLaw` : Spatial constancy of the Bernoulli function at each time.
+
+## iii. Table of contents
+
+- A. Bernoulli data
+- B. Conservative-force convention
+- C. Flow-state predicates
+- D. Bernoulli function
+- E. Bernoulli-law predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open scoped InnerProductSpace
+open Space
+open Time
+
+namespace FluidDynamics
+
+/-!
+
+## A. Bernoulli data
+
+-/
+
+/-- The fields needed for Bernoulli theory: Euler data, entropy, enthalpy, and an external
+potential.
+
+The potential is the potential energy per unit mass. In the conservative-force convention used
+below, it satisfies `bodyForce = -grad Phi`. This relation is not imposed by the data structure.
+-/
+structure FluidInBernoulliFlow (d : ℕ) extends FluidInEulerBalance d where
+  /-- The specific entropy field. -/
+  entropy : ScalarField d
+  /-- The specific enthalpy field. -/
+  enthalpy : ScalarField d
+  /-- The external potential field. -/
+  potential : Space d → ℝ
+
+/-!
+
+## B. Conservative-force convention
+
+-/
+
+/-- A Bernoulli flow has conservative body force when its body force is minus the gradient of
+the potential energy per unit mass. -/
+def HasConservativeBodyForce (d : ℕ) (data : FluidInBernoulliFlow d) : Prop :=
+  ∀ t x, data.bodyForce t x = -(∇ data.potential x)
+
+/-!
+
+## C. Flow-state predicates
+
+-/
+
+/-- A fluid state is steady when the velocity has zero time derivative everywhere. -/
+def IsSteady (d : ℕ) (fluid : FluidState d) : Prop :=
+  ∀ t x, ∂ₜ (fluid.velocity · x) t = 0
+
+/-- The material derivative `D_t f = partial_t f + u · grad f` of a scalar field. -/
+noncomputable def materialDerivative (d : ℕ) (fluid : FluidState d)
+    (field : ScalarField d) : ScalarField d :=
+  fun t x => ∂ₜ (field · x) t + ⟪fluid.velocity t x, ∇ (field t) x⟫_ℝ
+
+/-- A Bernoulli flow is isentropic when the entropy is materially conserved. -/
+def IsIsentropic (d : ℕ) (data : FluidInBernoulliFlow d) : Prop :=
+  ∀ t x, materialDerivative d data.toFluidState data.entropy t x = 0
+
+/-!
+
+## D. Bernoulli function
+
+-/
+
+/-- The specific kinetic energy `|u|^2 / 2` of a fluid state. -/
+noncomputable def specificKineticEnergy (d : ℕ) (fluid : FluidState d) : ScalarField d :=
+  fun t x => (1 / 2 : ℝ) * ⟪fluid.velocity t x, fluid.velocity t x⟫_ℝ
+
+/-- The Bernoulli function `|u|^2 / 2 + h + Phi`. -/
+noncomputable def bernoulliFunction (d : ℕ) (data : FluidInBernoulliFlow d) : ScalarField d :=
+  fun t x => specificKineticEnergy d data.toFluidState t x + data.enthalpy t x +
+    data.potential x
+
+/-!
+
+## E. Bernoulli-law predicates
+
+-/
+
+/-- A local Bernoulli law: the Bernoulli function has zero spatial gradient. -/
+def LocalBernoulliLaw (d : ℕ) (data : FluidInBernoulliFlow d) : Prop :=
+  ∀ t x, (∇ (bernoulliFunction d data t)) x = 0
+
+/-- A global Bernoulli law: the Bernoulli function is spatially constant at each time. -/
+def BernoulliLaw (d : ℕ) (data : FluidInBernoulliFlow d) : Prop :=
+  ∀ t x y, bernoulliFunction d data t x = bernoulliFunction d data t y
+
+end FluidDynamics

Physlib/FluidDynamics/Incompressible.lean

@@ -0,0 +1,79 @@
+/-
+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.FluidState
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+
+# Incompressible fluid flows
+
+## i. Overview
+
+This module defines general incompressibility predicates for fluid flows. These predicates are
+not tied to a particular equation of motion, so they can be reused later by incompressible
+Navier-Stokes, incompressible Euler, and Bernoulli-style developments.
+
+## ii. Key results
+
+- `incompressibilityResidual` : The divergence of the velocity field.
+- `ClassicalIncompressible` : Incompressibility guarded by velocity differentiability.
+- `SmoothIncompressible` : Incompressibility with globally differentiable velocity.
+- `SmoothIncompressible.toClassical` : Smooth incompressibility implies classical
+  incompressibility.
+- `DensityTimeIndependent` : A fluid flow whose density has zero time derivative.
+
+## iii. Table of contents
+
+- A. Incompressibility predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+
+/-!
+
+## A. Incompressibility predicates
+
+-/
+
+/-- The incompressibility residual, given by the divergence of the velocity field. -/
+noncomputable def incompressibilityResidual (d : ℕ) (fluid : FluidState d) :
+    Time → Space d → ℝ :=
+  fun t x => (∇ ⬝ fluid.velocity t) x
+
+/-- A classical incompressible flow has divergence-free velocity at points where the velocity
+field is differentiable. -/
+def ClassicalIncompressible (d : ℕ) (fluid : FluidState d) : Prop :=
+  ∀ t x, DifferentiableAt ℝ (fluid.velocity t) x →
+    incompressibilityResidual d fluid t x = 0
+
+/-- A smooth incompressible flow has globally differentiable velocity and vanishing
+incompressibility residual everywhere. -/
+def SmoothIncompressible (d : ℕ) (fluid : FluidState d) : Prop :=
+  (∀ t, Differentiable ℝ (fluid.velocity t)) ∧
+    ∀ t x, incompressibilityResidual d fluid t x = 0
+
+/-- A smooth incompressible flow is classically incompressible. -/
+lemma SmoothIncompressible.toClassical (d : ℕ) (fluid : FluidState d) :
+    SmoothIncompressible d fluid → ClassicalIncompressible d fluid := by
+  intro hSmooth t x _
+  simpa [incompressibilityResidual] using hSmooth.2 t x
+
+/-- A fluid flow has time-independent density when the density has zero time derivative at
+each spatial point. -/
+def DensityTimeIndependent (d : ℕ) (fluid : FluidState d) : Prop :=
+  ∀ t x, ∂ₜ (fluid.rho · x) t = 0
+
+end FluidDynamics