Physlib.FluidDynamics.CauchyFlow.Momentum

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.CauchyFlow.Basic
public import Physlib.FluidDynamics.FluidFlow.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

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.momentumDensity d flow.toFluidFlow · x) t +
        matrixDiv d (FluidFlow.momentumFlux 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).


lemma 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 := byd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow
  have conservative_eq_convective_lhs : ∀ t x,
      ∂ₜ (FluidFlow.momentumDensity d flow.toFluidFlow · x) t +
          matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
        flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x := by
    intro t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space d⊢ ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
    matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow
    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := byd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flowd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
    matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow
      simpa [FluidFlow.continuityResidual] using
        hContinuity t x (byd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) td:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
    matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow simpa using hRhoTime t xAll goals completed! 🐙d:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
    matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow) (hMomentumDensity t).differentiableAtd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
    matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow
    rw [FluidFlow.momentumTransport_eq_materialAcceleration_add_continuityResidual
        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)
        (hMomentumDensity t) (hVelocitySpace t),d:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x +
    FluidFlow.continuityResidual d flow.toFluidFlow t x • flow.velocity t x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow hResidual,d:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x + 0 • flow.velocity t x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow zero_smul,d:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x + 0 =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow add_zerod:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)t:Timex:Space dhResidual:FluidFlow.continuityResidual d flow.toFluidFlow t x = 0⊢ flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x =
  flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t xd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow]d:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flowd:ℕflow:CauchyFlow dhContinuity:FluidFlow.ClassicalContinuityEquation d flow.toFluidFlowhRhoTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.rho x_1 x) thVelocityTime:∀ (t : Time) (x : Space d), DifferentiableAt ℝ (fun x_1 => flow.velocity x_1 x) thMomentumDensity:∀ (t : Time), Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t)hVelocitySpace:∀ (t : Time), Differentiable ℝ (flow.velocity t)conservative_eq_convective_lhs:∀ (t : Time) (x : Space d),
  ∂ₜ (fun x_1 => FluidFlow.momentumDensity d flow.toFluidFlow x_1 x) t +
      matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x⊢ CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow
  exact ⟨fun h t x => (conservative_eq_convective_lhs t x).symm.trans (h t x),
    fun h t x => (conservative_eq_convective_lhs t x).trans (h t x)⟩All goals completed! 🐙