Imports
/-
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.FluidFlow.Continuity
public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDivMomentum fields for fluid flows
i. Overview
This module defines generic momentum fields for fluid flow and relates conservative momentum transport to mass density times material acceleration. The definitions do not choose a particular force law or stress model, so they can be reused by Navier-Stokes, Euler, and related systems.
ii. Key results
FluidFlow.momentumDensity : The vector momentum density rho u.
FluidFlow.momentumFlux : The convective momentum flux rho u ⊗ u.
FluidFlow.convectiveTerm : The nonlinear transport term (u · ∇)u.
FluidFlow.materialAcceleration : The material acceleration ∂ₜ u + (u · ∇)u.
FluidFlow.momentumTransport_eq_materialAcceleration_add_continuityResidual :
The momentum-transport identity relating conservative and convective quantities.
iii. Table of contents
A. Momentum fields
B. Momentum transport identity
iv. References
@[expose] public sectionA. Momentum fields
The momentum density rho u.
def momentumDensity (d : ℕ) (fluid : FluidFlow d) : MomentumDensityField d :=
fun t x => fluid.rho t x • fluid.velocity t x
The convective momentum flux rho u ⊗ u.
def momentumFlux (d : ℕ) (fluid : FluidFlow d) : Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
fun t x =>
fluid.rho t x • Matrix.vecMulVec (fun i => fluid.velocity t x i)
(fun j => fluid.velocity t x j)B. Momentum transport identity
Product rule for the time derivative of a scalar field times a velocity field.
d:ℕrhoAtPosition:Time → ℝvelocityAtPosition:Time → EuclideanSpace ℝ (Fin d)t:TimehRho:DifferentiableAt ℝ rhoAtPosition thVelocity:DifferentiableAt ℝ velocityAtPosition t⊢ (rhoAtPosition t • fderiv ℝ velocityAtPosition t + (fderiv ℝ rhoAtPosition t).smulRight (velocityAtPosition t)) 1 =
rhoAtPosition t • (fderiv ℝ velocityAtPosition t) 1 + (fderiv ℝ rhoAtPosition t) 1 • velocityAtPosition t
All goals completed! 🐙
Product rule for the time derivative of the momentum density rho u.
lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidFlow d)
(t : Time) (x : Space d)
(hRho : DifferentiableAt ℝ (fluid.rho · x) t)
(hVelocity : DifferentiableAt ℝ (fluid.velocity · x) t) :
∂ₜ (momentumDensity d fluid · x) t =
fluid.rho t x • ∂ₜ (fluid.velocity · x) t + ∂ₜ (fluid.rho · x) t • fluid.velocity t x := d:ℕfluid:FluidFlow dt:Timex:Space dhRho:DifferentiableAt ℝ (fun x_1 => fluid.rho x_1 x) thVelocity:DifferentiableAt ℝ (fun x_1 => fluid.velocity x_1 x) t⊢ ∂ₜ (fun x_1 => momentumDensity d fluid x_1 x) t =
fluid.rho t x • ∂ₜ (fun x_1 => fluid.velocity x_1 x) t + ∂ₜ (fun x_1 => fluid.rho x_1 x) t • fluid.velocity t x
All goals completed! 🐙
Product rule for one spatial derivative of one component of rho u ⊗ u.
d:ℕfluid:FluidFlow dt:Timex:Space di:Fin dj:Fin dhMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocity:Differentiable ℝ (fluid.velocity t)hProduct:Space.deriv j ((fun x' => (fluid.velocity t x').ofLp i) • fun x' => (momentumDensity d fluid t x').ofLp j) x =
(fluid.velocity t x).ofLp i • Space.deriv j (fun x' => (momentumDensity d fluid t x').ofLp j) x +
Space.deriv j (fun x' => (fluid.velocity t x').ofLp i) x • (momentumDensity d fluid t x).ofLp j⊢ Space.deriv j (fun x' => momentumFlux d fluid t x' i j) x =
Space.deriv j ((fun x' => (fluid.velocity t x').ofLp i) • fun x' => (momentumDensity d fluid t x').ofLp j) x
d:ℕfluid:FluidFlow dt:Timex:Space di:Fin dj:Fin dhMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocity:Differentiable ℝ (fluid.velocity t)hProduct:Space.deriv j ((fun x' => (fluid.velocity t x').ofLp i) • fun x' => (momentumDensity d fluid t x').ofLp j) x =
(fluid.velocity t x).ofLp i • Space.deriv j (fun x' => (momentumDensity d fluid t x').ofLp j) x +
Space.deriv j (fun x' => (fluid.velocity t x').ofLp i) x • (momentumDensity d fluid t x).ofLp j⊢ (fun x' => momentumFlux d fluid t x' i j) =
(fun x' => (fluid.velocity t x').ofLp i) • fun x' => (momentumDensity d fluid t x').ofLp j
d:ℕfluid:FluidFlow dt:Timex:Space di:Fin dj:Fin dhMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocity:Differentiable ℝ (fluid.velocity t)hProduct:Space.deriv j ((fun x' => (fluid.velocity t x').ofLp i) • fun x' => (momentumDensity d fluid t x').ofLp j) x =
(fluid.velocity t x).ofLp i • Space.deriv j (fun x' => (momentumDensity d fluid t x').ofLp j) x +
Space.deriv j (fun x' => (fluid.velocity t x').ofLp i) x • (momentumDensity d fluid t x).ofLp jx':Space d⊢ momentumFlux d fluid t x' i j =
((fun x' => (fluid.velocity t x').ofLp i) • fun x' => (momentumDensity d fluid t x').ofLp j) x'
All goals completed! 🐙
The matrix divergence of rho u ⊗ u split into continuity and convective parts.
d:ℕfluid:FluidFlow dt:Timex:Space dhMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocity:Differentiable ℝ (fluid.velocity t)i:Fin dj:Fin da✝:j ∈ Finset.univ⊢ (Space.deriv j (fun x => fluid.velocity t x) x).ofLp i * (momentumDensity d fluid t x).ofLp j =
fluid.rho t x * ((fluid.velocity t x).ofLp j * (Space.deriv j (fluid.velocity t) x).ofLp i)
All goals completed! 🐙
_ = (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) * fluid.velocity t x i +
fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := d:ℕfluid:FluidFlow dt:Timex:Space dhMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocity:Differentiable ℝ (fluid.velocity t)i:Fin d⊢ (fluid.velocity t x).ofLp i * ∑ j, Space.deriv j (fun x' => (momentumDensity d fluid t x').ofLp j) x +
fluid.rho t x * ∑ j, (fluid.velocity t x).ofLp j * (Space.deriv j (fluid.velocity t) x).ofLp i =
(∑ j, Space.deriv j (fun x' => (momentumDensity d fluid t x').ofLp j) x) * (fluid.velocity t x).ofLp i +
fluid.rho t x * ∑ j, (fluid.velocity t x).ofLp j * (Space.deriv j (fluid.velocity t) x).ofLp i
All goals completed! 🐙The conservative momentum transport terms equal mass density times material acceleration plus the continuity residual times velocity.
d:ℕfluid:FluidFlow dt:Timex:Space dhRhoTime:DifferentiableAt ℝ (fun x_1 => fluid.rho x_1 x) thVelocityTime:DifferentiableAt ℝ (fun x_1 => fluid.velocity x_1 x) thMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocitySpace:Differentiable ℝ (fluid.velocity t)⊢ fluid.rho t x • ∂ₜ (fun x_1 => fluid.velocity x_1 x) t + ∂ₜ (fun x_1 => fluid.rho x_1 x) t • fluid.velocity t x +
(div (momentumDensity d fluid t) x • fluid.velocity t x + fluid.rho t x • convectiveTerm d fluid t x) =
fluid.rho t x • materialAcceleration d fluid t x +
(∂ₜ (fun x_1 => fluid.rho x_1 x) t + div (fun x' => fluid.rho t x' • fluid.velocity t x') x) • fluid.velocity t x
d:ℕfluid:FluidFlow dt:Timex:Space dhRhoTime:DifferentiableAt ℝ (fun x_1 => fluid.rho x_1 x) thVelocityTime:DifferentiableAt ℝ (fun x_1 => fluid.velocity x_1 x) thMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocitySpace:Differentiable ℝ (fluid.velocity t)i:Fin d⊢ (fluid.rho t x • ∂ₜ (fun x_1 => fluid.velocity x_1 x) t + ∂ₜ (fun x_1 => fluid.rho x_1 x) t • fluid.velocity t x +
(div (momentumDensity d fluid t) x • fluid.velocity t x + fluid.rho t x • convectiveTerm d fluid t x)).ofLp
i =
(fluid.rho t x • materialAcceleration d fluid t x +
(∂ₜ (fun x_1 => fluid.rho x_1 x) t + div (fun x' => fluid.rho t x' • fluid.velocity t x') x) •
fluid.velocity t x).ofLp
i
d:ℕfluid:FluidFlow dt:Timex:Space dhRhoTime:DifferentiableAt ℝ (fun x_1 => fluid.rho x_1 x) thVelocityTime:DifferentiableAt ℝ (fun x_1 => fluid.velocity x_1 x) thMomentumDensity:Differentiable ℝ (momentumDensity d fluid t)hVelocitySpace:Differentiable ℝ (fluid.velocity t)i:Fin d⊢ fluid.rho t x * (∂ₜ (fun x_1 => fluid.velocity x_1 x) t).ofLp i +
∂ₜ (fun x_1 => fluid.rho x_1 x) t * (fluid.velocity t x).ofLp i +
((∑ x_1, Space.deriv x_1 (fun x => fluid.rho t x * (fluid.velocity t x).ofLp x_1) x) * (fluid.velocity t x).ofLp i +
fluid.rho t x * ∑ x_1, (fluid.velocity t x).ofLp x_1 * (Space.deriv x_1 (fluid.velocity t) x).ofLp i) =
fluid.rho t x * (∂ₜ (fun x_1 => fluid.velocity x_1 x) t).ofLp i +
fluid.rho t x * ∑ x_1, (fluid.velocity t x).ofLp x_1 * (Space.deriv x_1 (fluid.velocity t) x).ofLp i +
(∂ₜ (fun x_1 => fluid.rho x_1 x) t +
∑ x_1, Space.deriv x_1 (fun x => fluid.rho t x * (fluid.velocity t x).ofLp x_1) x) *
(fluid.velocity t x).ofLp i
All goals completed! 🐙