Physlib.FluidDynamics.CauchyFlow.Inviscid

Imports

/-
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.CauchyFlow.Basic
public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv

Inviscid stress laws for Cauchy flows

i. Overview

This module defines the inviscid stress law for CauchyFlow and the corresponding matrix-divergence identity for pressure stress.

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.

iii. Table of contents

A. Inviscid stress law

iv. References

@[expose] public section

A. Inviscid stress law

A Cauchy flow is inviscid with pressure p when its stress is the isotropic pressure stress -p I.

In this formulation, inviscid means that the Cauchy stress has no viscous or shear contribution. It does not rule out body forces; those are carried separately by CauchyFlow.specificBodyForce.

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 := byd:ℕpressureAtTime:Space d → ℝ⊢ (matrixDiv d fun x => -pressureAtTime x • 1) = -∇ pressureAtTime
  ext x id:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ (matrixDiv d (fun x => -pressureAtTime x • 1) x).ofLp i = ((-∇ pressureAtTime) x).ofLp i
  rw [matrixDiv_applyd:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∑ j, Space.deriv j (fun x => (-pressureAtTime x • 1) i j) x = ((-∇ pressureAtTime) x).ofLp id:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∑ j, Space.deriv j (fun x => (-pressureAtTime x • 1) i j) x = ((-∇ pressureAtTime) x).ofLp i]d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∑ j, Space.deriv j (fun x => (-pressureAtTime x • 1) i j) x = ((-∇ pressureAtTime) x).ofLp i
  rw [Finset.sum_eq_single id:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = ((-∇ pressureAtTime) x).ofLp ih₀d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → Space.deriv b (fun x => (-pressureAtTime x • 1) i b) x = 0h₁d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ i ∉ Finset.univ → Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = 0d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = ((-∇ pressureAtTime) x).ofLp ih₀d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → Space.deriv b (fun x => (-pressureAtTime x • 1) i b) x = 0h₁d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ i ∉ Finset.univ → Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = 0]d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = ((-∇ pressureAtTime) x).ofLp ih₀d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → Space.deriv b (fun x => (-pressureAtTime x • 1) i b) x = 0h₁d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ i ∉ Finset.univ → Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = 0
  ·d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = ((-∇ pressureAtTime) x).ofLp i simp [grad, Space.deriv_eq]All goals completed! 🐙
  ·h₀d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → Space.deriv b (fun x => (-pressureAtTime x • 1) i b) x = 0 intro j _ hjih₀d:ℕpressureAtTime:Space d → ℝx:Space di:Fin dj:Fin da✝:j ∈ Finset.univhji:j ≠ i⊢ Space.deriv j (fun x => (-pressureAtTime x • 1) i j) x = 0
    have hij : i ≠ j := fun h => hji h.symmh₀d:ℕpressureAtTime:Space d → ℝx:Space di:Fin dj:Fin da✝:j ∈ Finset.univhji:j ≠ ihij:i ≠ j⊢ Space.deriv j (fun x => (-pressureAtTime x • 1) i j) x = 0
    simp [hij]All goals completed! 🐙
  ·h₁d:ℕpressureAtTime:Space d → ℝx:Space di:Fin d⊢ i ∉ Finset.univ → Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = 0 intro hih₁d:ℕpressureAtTime:Space d → ℝx:Space di:Fin dhi:i ∉ Finset.univ⊢ Space.deriv i (fun x => (-pressureAtTime x • 1) i i) x = 0
    simp at hiAll goals completed! 🐙

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) := byd:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressure⊢ ∀ (t : Time), matrixDiv d (flow.stress t) = -∇ (pressure t)
  intro td:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressuret:Time⊢ matrixDiv d (flow.stress t) = -∇ (pressure t)
  rw [show flow.stress t =
      fun x => (-(pressure t x)) • (1 : Matrix (Fin d) (Fin d) ℝ) byd:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressure⊢ ∀ (t : Time), matrixDiv d (flow.stress t) = -∇ (pressure t)d:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressuret:Time⊢ (matrixDiv d fun x => -pressure t x • 1) = -∇ (pressure t)
    funext xd:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressuret:Timex:Space d⊢ flow.stress t x = -pressure t x • 1d:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressuret:Time⊢ (matrixDiv d fun x => -pressure t x • 1) = -∇ (pressure t)
    exact hInviscid t xAll goals completed! 🐙d:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressuret:Time⊢ (matrixDiv d fun x => -pressure t x • 1) = -∇ (pressure t)]d:ℕflow:CauchyFlow dpressure:ScalarField dhInviscid:IsInviscid d flow pressuret:Time⊢ (matrixDiv d fun x => -pressure t x • 1) = -∇ (pressure t)
  exact matrixDiv_inviscid_pressure_stress d (pressure t)All goals completed! 🐙