Initial IdealFluid structure

Physlib.lean

@@ -80,6 +80,10 @@ public import Physlib.Mathematics.VariationalCalculus.HasVarAdjoint
 public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
 public import Physlib.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
 public import Physlib.Mathematics.VariationalCalculus.IsTestFunction
+public import Physlib.FluidMechanics.IdealFluids.Basic
+public import Physlib.FluidMechanics.IdealFluids.Bernoulli
+public import Physlib.FluidMechanics.IdealFluids.Continuity
+public import Physlib.FluidMechanics.IdealFluids.Euler
 public import Physlib.Meta.AllFilePaths
 public import Physlib.Meta.Basic
 public import Physlib.Meta.Informal.Basic

Physlib/FluidMechanics/IdealFluids/Basic.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+
+module
+
+public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Mathlib.Analysis.Calculus.ContDiff.Basic
+public import Physlib.SpaceAndTime.Space.Module
+public import Physlib.SpaceAndTime.Time.Basic
+
+/-!
+This module introduces the idea of an ideal fluid and the mass flux density
+and basic physical properties, meant to be later used for proofs.
+-/
+
+open scoped InnerProductSpace
+
+/-- Introducing the structure of Ideal Fluids -/
+public structure IdealFluid where
+  /-- The density at a specific point and time -/
+  density: Time → Space → ℝ
+  /-- The velocity at a specific point and time -/
+  velocity: Time → Space → EuclideanSpace ℝ (Fin 3)
+  /-- The pressure at a specific point and time -/
+  pressure: Time → Space → ℝ
+  /-- The entropy at a specific point and time -/
+  entropy: Time → Space → ℝ
+  /-- The enthalpy at a specific point and time -/
+  enthalpy: Time → Space → ℝ
+
+  density_pos: ∀ t pos, 0 < density t pos
+
+  /-- Ensuring that all are differentiable for more complex equations. -/
+  density_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>density s.1 s.2)
+  velocity_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>velocity s.1 s.2)
+  pressure_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>pressure s.1 s.2)
+
+  entropy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>entropy s.1 s.2)
+  enthalpy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthalpy s.1 s.2)
+
+namespace IdealFluid
+open MeasureTheory
+
+/-- Mass flux density j=ρv -/
+public abbrev massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+      F.density t pos • F.velocity t pos
+
+/-- Entropy flux density ρsv -/
+public abbrev entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+      (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+
+/-- Energy flux density ρv(1/2 |v|^2 + w) -/
+noncomputable abbrev energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+      let w := IdealFluid.enthalpy F t pos
+      let v := IdealFluid.velocity F t pos
+      let v_sq: ℝ := ⟪v,v⟫_ℝ
+      let scalar := (IdealFluid.density F t pos)*(0.5*v_sq + w)
+
+      scalar • v
+
+/-- Volume to introduce surface integrals -/
+structure FluidVolume where
+  /-- The 3D region -/
+  region: Set Space
+  /-- The normal pointing outwards -/
+  normal: Space → EuclideanSpace ℝ (Fin 3)
+  /-- 2D measure of the boundary -/
+  surfaceMeasure: Measure Space
+
+/-- Surface integral of a vector field -/
+noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpace ℝ (Fin 3)):
+    ℝ :=
+      ∫ (pos: Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
+
+/-- Mass flow out of volume -/
+noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (IdealFluid.massFluxDensity F t ·)
+
+/-- Entropy flow out of volume -/
+noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (IdealFluid.entropyFluxDensity F t ·)
+
+/-- Energy flow out of volume -/
+noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (IdealFluid.energyFluxDensity F t ·)
+
+end IdealFluid

Physlib/FluidMechanics/IdealFluids/Bernoulli.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+
+module
+
+public import Physlib.FluidMechanics.IdealFluids.Basic
+public import Physlib.FluidMechanics.IdealFluids.Euler
+public import Physlib.Mathematics.Calculus.Divergence
+public import Physlib.SpaceAndTime.Time.Derivatives
+
+/-!
+This module introduces:
+steady flow,
+... (still under construction)
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+/-- Determines whether a flow is steady -/
+def IdealFluid.isSteady (F: IdealFluid) :
+    Prop :=
+      ∀ (pos : Space),
+      ∂ₜ (F.velocity · pos) = 0
+
+/-- Definition of a material derivative -/
+noncomputable def IdealFluid.materialDerivative (t: Time) (pos: Space)
+(F: IdealFluid) (f: Time → Space → ℝ) :
+    ℝ :=
+      ∂ₜ (f · pos) t +
+      ⟪F.velocity t pos, ∇ (f t ·) pos ⟫_ℝ
+
+/-- Determines whether a flow is isentropic -/
+def IdealFluid.isIsentropic (F: IdealFluid):
+    Prop :=
+      ∀ (t: Time) (pos: Space),
+      F.materialDerivative t pos F.entropy = 0
+
+-- TODO: Make into material derivative
+
+/-- The Bernoulli function (1/2)v^2 + w -/
+noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
+(t: Time) (pos: Space) (g: Space → ℝ):
+    ℝ :=
+      let v := F.velocity t pos
+      0.5 * ⟪v, v⟫_ℝ + F.enthalpy t pos + g pos
+
+-- TODO: Recheck sign
+
+/-- Derivation:
+  If the flow is steady and isentropic, the bernoulli equation is constant
+-/
+theorem bernoulli_derivation (F : IdealFluid) (g : Space → ℝ) (t : Time) (pos : Space)
+    (Eul : F.satisfiesEuler g)
+    (Stdy : F.isSteady)
+    (Istrpc : F.isIsentropic) :
+    let v := F.velocity t pos
+    ⟪v, Space.grad (F.bernoulliEquation t · g) pos⟫_ℝ = 0 :=
+      by
+        sorry

Physlib/FluidMechanics/IdealFluids/Continuity.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+
+module
+
+public import Physlib.FluidMechanics.IdealFluids.Basic
+public import Physlib.Mathematics.Calculus.Divergence
+public import Physlib.SpaceAndTime.Time.Derivatives
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+
+/-!
+This module introduces the continuity criterium.
+There is potential to add various different lemmas expanding on this.
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+/-- defining satisfying the equation of continuity -/
+public def IdealFluid.satisfiesContinuity (F : IdealFluid):
+    Prop :=
+      ∀ (t : Time) (pos : Space),
+      ∂ₜ (F.density · pos) t +
+      Space.div (F.massFluxDensity t ·) pos = (0 : ℝ)
+
+/-- Criterion for incompressibility -/
+public def IdealFluid.isIncompressible (F : IdealFluid):
+    Prop :=
+      ∀ (t : Time) (pos : Space), ∂ₜ (F.density · pos) t = 0
+
+/-- Theorem: If constant density and incompressible div(v)=0-/
+theorem incompress_const_density_implies_div_v_eq_zero (F : IdealFluid)
+    (Cont      : F.satisfiesContinuity)
+    (Incomp    : F.isIncompressible)
+    (ConstDens : ∀ (t : Time) (pos : Space), Space.grad (F.density t ·) pos = 0) :
+    ∀ (t : Time) (pos : Space), Space.div (F.velocity t ·) pos = 0 := by
+      sorry

Physlib/FluidMechanics/IdealFluids/Euler.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+
+module
+
+public import Physlib.FluidMechanics.IdealFluids.Basic
+public import Physlib.Mathematics.Calculus.Divergence
+public import Physlib.SpaceAndTime.Time.Derivatives
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+
+/-!
+This module introduces the Euler's equation.
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+/-- Defines the property of satisfying Euler's equation. -/
+public def IdealFluid.satisfiesEuler (F: IdealFluid) (g: Space → ℝ):
+    Prop :=
+      ∀ (t : Time) (pos : Space),
+        let v := F.velocity t pos
+        ∂ₜ (F.velocity · pos) t +
+        (fun i => ⟪v, Space.grad (F.velocity t · i) pos⟫_ℝ)
+        = -(1/F.density t pos) • Space.grad (F.pressure t ·) pos + Space.grad g pos