Bernoulli's Principle

Stream: Natural sciences

[Bulhwi Cha]

Bulhwi Cha said:

I should also point out that David⚛️'s formalization of the Darcy-Weisbach equation has the same problem. Where's the definition of force? Premises like h₃ : F = f₁ * P * L * U^2 are not definitions. These formalizations are all underspecifications!

Tomas Skrivan said:

I'm looking forward to seeing a refactored version where it is clear what are the assumptions, definitions and empirical facts!

@Tomas Skrivan I also want to hear your thoughts on this matter.

[Tomas Skrivan]

I'm not entirely sure what to say as I didn't have time to fully understand the DW equation yet.

However, Bernoulli principle can be formally derived for potential flow satisfying the Euler equation(Navier-Stokes with zero viscosity).

Therefore anything using the Bernoulli principle should be framed in the context of potential flow and I do not see potential flow mentioned anywhere.

[Tomas Skrivan]

Here is my sketch of formalizing Bernoulli's principle. I skipped proofs but I think that it should be fairly straightforward for someone familiar with relevant parts of mathlib.

[Tomas Skrivan]

edit: fixed ℝ³ based on Eric's suggestion

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

open BigOperators

notation " ℝ³ " => EuclideanSpace ℝ (Fin 3)

variable {X : Type _} [NormedAddCommGroup X] [NormedSpace ℝ X]

def basis (i : Fin 3) : ℝ³ := fun j => if i=j then 1 else 0

/-- Partial derivative -/
noncomputable
def pderiv (i : Fin 3) (f : ℝ³ → X) : ℝ³ → X :=
  fun x => fderiv ℝ (fun h : ℝ => f (x + h • basis i)) 0 1

def StationaryFlow (v : ℝ → ℝ³ → ℝ³) := ∀ t x, v t x = v 0 x
def PotentialFlow   (v : ℝ → ℝ³ → ℝ³) := ∃ φ : ℝ → ℝ³ → ℝ, ∀ t x i, pderiv i (φ t) x = v t x i

/-- Potential flow identity 1 `(v⬝∇)v = (∇v)^T v` -/
theorem potential_flow_identity1 (v : ℝ → ℝ³ → ℝ³)
  : PotentialFlow v → ∀ t x i,
    (∑ j, v t x j * pderiv j (v t · i) x)
    =
    (∑ j, v t x j * pderiv i (v t · j) x)
  := sorry
    -- rewrite `v = ∇ φ` and swap partial derivatives

/-- Potential flow identity 2  `(v⬝∇)v = 1/2 * ∇ ‖v‖²` -/
theorem potential_flow_identity2 (v : ℝ → ℝ³ → ℝ³)
  : PotentialFlow v →
      ∀ t x i,
      (∑ j, v t x j * pderiv j (v t · i) x)
      =
      1/2 * pderiv i (‖v t ·‖^2) x
  := sorry
    -- 1. differentiate through the norm
    -- 2. expand definition of the inner product
    -- 3. apply potential_flow_identity1


def EulerEquation (v : ℝ → ℝ³ → ℝ³) (p : ℝ → ℝ³ → ℝ) (forces : ℝ → ℝ³ → ℝ³) :=
  ∀ t x i,
    -- ∂v/∂t               + (v⬝∇)v                                + ∇p                 + f = 0
    fderiv ℝ (v · x i) t 1 + (∑ j, v t x j * pderiv j (v t · i) x) + pderiv i (p t ·) x  - forces t x i= 0


/-- Function with zero derivative everywhere is constant -/
def zero_pderiv_is_const (f : ℝ³ → X)
  : (∀ x i, pderiv i f x = 0) → ∃ c, ∀ x, f x = c := sorry


def BernoulliPrinciple
  (v : ℝ → ℝ³ → ℝ³) (p : ℝ → ℝ³ → ℝ)
  (V : ℝ → ℝ³ → ℝ) -- external forces potential
  : StationaryFlow v →
    PotentialFlow v →
    EulerEquation v p (fun t x i => - pderiv i (V t ·) x) →
    ∃ c, ∀ t x, 1/2 * ‖v t x‖^2 + p t x + V t x = c
  := sorry
  -- 1. stationary flow implies `∂v/∂t = 0`
  -- 2. potential flow implies  `(v⬝∇)v = 1/2 * ∇ ‖v‖²`
  -- 3. euler equation reduces to
  --    1/2 * ∇ ‖v‖² + ∇ p + ∇ V = 0
  -- 4. apply `zero_pderiv_is_const`

[Eric Wieser]

Note that in mathlib h • basis i is usually written Pi.single i h

[Eric Wieser]

Warrning: Make sure that it is ‖·‖₂ norm and not ‖·‖∞ norm?

It's the wrong norm, you need docs#EuclideanSpace (notation " ℝ³ " => EuclideanSpace (Fin 3) ℝ)

[Notification Bot]

6 messages were moved here from #Natural sciences > wrong formalization of boyle's law in lean by Tyler Josephson ⚛️.

[Tyler Josephson ⚛️]

I like this! Indeed, Bernoulli's principle seems to apply only when viscous forces are negligible. @David⚛️'s use of Bernoulli's principle in the Darcy-Weisbach equation is given in this way:

(h₀: H_loss = p₁/(ρ*g) + u₁^2 /(2*g) + z₁ - p₂/(ρ*g) - u₂^2 /(2*g) - z₂)

Maybe this is where the "semi-empirical" part comes in? Bernoulli's principle is for the case in which H_loss = 0, or

p/(ρ*g) + u^2 /(2*g) + z = constant

To connect a formally-derived Bernoulli's principle to the first equation, used in deriving Darcy-Weisbach, we'd need to figure out a way to smuggle a H_loss term in, maybe by way of an additional hypothesis.

[Tomas Skrivan]

Finally I have a little bit of understanding of the DW equation. You can analytically derive it from Navier-Stokes equation for laminar flow. In that case, it is known as Hagen–Poiseuille law. This should be easy to formalize.

The empirical part is that the formula holds for other flows if you modify the viscosity based on the turbulence. There seems to be different empirical modifications based on the type of the flow. Actually, I do not see the connection between Bernoulli's principle and DW equation as one is talking about inviscid flow and the other about viscid flow. And I don't see how this can be formalized.

[David⚛️]

Tomas Skrivan said:

Finally I have a little bit of understanding of the DW equation. You can analytically derive it from Navier-Stokes equation for laminar flow. In that case, it is known as Hagen–Poiseuille law. This should be easy to formalize.

The empirical part is that the formula holds for other flows if you modify the viscosity based on the turbulence. There seems to be different empirical modifications based on the type of the flow. Actually, I do not see the connection between Bernoulli's principle and DW equation as one is talking about inviscid flow and the other about viscid flow. And I don't see how this can be formalized.

Yes, there is a connection between the Darcy-Weisbach equation and Bernoulli’s equation. The Darcy-Weisbach equation is used to calculate the head loss due to friction in a pipe. Bernoulli’s equation is used to calculate the pressure drop due to a change in the velocity of a fluid. The two equations are related because the head loss due to friction can be expressed as a function of the velocity of the fluid. This relationship is used to derive the Darcy-Weisbach equation from Bernoulli’s equation

[David⚛️]

@Tomas Skrivan The Darcy-Weisbach equation is commonly used to calculate the head loss or pressure drop in a pipe due to friction. It is based on the principle that energy is dissipated as fluid flows through a pipe, resulting in a loss of pressure. The connection between the Darcy-Weisbach equation and the Bernoulli equation lies in the fact that the head loss due to friction in the Darcy-Weisbach equation represents a form of energy dissipation.
It is important to note that the Bernoulli equation does not explicitly account for head loss due to friction, whereas the Darcy-Weisbach equation is specifically designed to calculate this loss. By considering the connection between these equations, engineers can analyze fluid flow systems, taking into account both pressure changes due to potential energy and the effects of frictional losses.

[Max Bobbin]

Tomas Skrivan said:

edit: fixed ℝ³ based on Eric's suggestion

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

open BigOperators

notation " ℝ³ " => EuclideanSpace ℝ (Fin 3)

variable {X : Type _} [NormedAddCommGroup X] [NormedSpace ℝ X]

def basis (i : Fin 3) : ℝ³ := fun j => if i=j then 1 else 0

/-- Partial derivative -/
noncomputable
def pderiv (i : Fin 3) (f : ℝ³ → X) : ℝ³ → X :=
  fun x => fderiv ℝ (fun h : ℝ => f (x + h • basis i)) 0 1

def StationaryFlow (v : ℝ → ℝ³ → ℝ³) := ∀ t x, v t x = v 0 x
def PotentialFlow   (v : ℝ → ℝ³ → ℝ³) := ∃ φ : ℝ → ℝ³ → ℝ, ∀ t x i, pderiv i (φ t) x = v t x i

/-- Potential flow identity 1 `(v⬝∇)v = (∇v)^T v` -/
theorem potential_flow_identity1 (v : ℝ → ℝ³ → ℝ³)
  : PotentialFlow v → ∀ t x i,
    (∑ j, v t x j * pderiv j (v t · i) x)
    =
    (∑ j, v t x j * pderiv i (v t · j) x)
  := sorry
    -- rewrite `v = ∇ φ` and swap partial derivatives

/-- Potential flow identity 2  `(v⬝∇)v = 1/2 * ∇ ‖v‖²` -/
theorem potential_flow_identity2 (v : ℝ → ℝ³ → ℝ³)
  : PotentialFlow v →
      ∀ t x i,
      (∑ j, v t x j * pderiv j (v t · i) x)
      =
      1/2 * pderiv i (‖v t ·‖^2) x
  := sorry
    -- 1. differentiate through the norm
    -- 2. expand definition of the inner product
    -- 3. apply potential_flow_identity1


def EulerEquation (v : ℝ → ℝ³ → ℝ³) (p : ℝ → ℝ³ → ℝ) (forces : ℝ → ℝ³ → ℝ³) :=
  ∀ t x i,
    -- ∂v/∂t               + (v⬝∇)v                                + ∇p                 + f = 0
    fderiv ℝ (v · x i) t 1 + (∑ j, v t x j * pderiv j (v t · i) x) + pderiv i (p t ·) x  - forces t x i= 0


/-- Function with zero derivative everywhere is constant -/
def zero_pderiv_is_const (f : ℝ³ → X)
  : (∀ x i, pderiv i f x = 0) → ∃ c, ∀ x, f x = c := sorry


def BernoulliPrinciple
  (v : ℝ → ℝ³ → ℝ³) (p : ℝ → ℝ³ → ℝ)
  (V : ℝ → ℝ³ → ℝ) -- external forces potential
  : StationaryFlow v →
    PotentialFlow v →
    EulerEquation v p (fun t x i => - pderiv i (V t ·) x) →
    ∃ c, ∀ t x, 1/2 * ‖v t x‖^2 + p t x + V t x = c
  := sorry
  -- 1. stationary flow implies `∂v/∂t = 0`
  -- 2. potential flow implies  `(v⬝∇)v = 1/2 * ∇ ‖v‖²`
  -- 3. euler equation reduces to
  --    1/2 * ∇ ‖v‖² + ∇ p + ∇ V = 0
  -- 4. apply `zero_pderiv_is_const`

still learning Lean4. What is fun? Example of using it here: fun h : ℝ => f (x + h • basis i)) 0 1 is it the same as the lambda operator in Lean3?

[Shreyas Srinivas]

Yes. In lean 4 you can still replace fun with lambda

[Shreyas Srinivas]

Although I think from a programmer's perspective, it will confuse a lot of newcomers.

[Tyler Josephson ⚛️]

By the way, is this pderiv used anywhere else? How does it work? (Been wanting partial derivatives for transport and thermodynamics for a long time)

[Tomas Skrivan]

I do not know how partial derivatives are done in mathlib. I just made this definition up, it is just a directional derivative in the coordinate direction.