Initial IdealFluid structure

PhysLean.lean

@@ -44,6 +44,10 @@ public import PhysLean.Electromagnetism.PointParticle.ThreeDimension
 public import PhysLean.Electromagnetism.Vacuum.Constant
 public import PhysLean.Electromagnetism.Vacuum.HarmonicWave
 public import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
+public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.FluidMechanics.IdealFluid.Bernoulli
+public import PhysLean.FluidMechanics.IdealFluid.Continuity
+public import PhysLean.FluidMechanics.IdealFluid.Euler
 public import PhysLean.Mathematics.Calculus.AdjFDeriv
 public import PhysLean.Mathematics.Calculus.Divergence
 public import PhysLean.Mathematics.DataStructures.FourTree.Basic

PhysLean/FluidMechanics/IdealFluid/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 PhysLean.SpaceAndTime.Space.Module
+public import PhysLean.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 (fun pos => IdealFluid.massFluxDensity F t pos)
+
+/-- Entropy flow out of volume -/
+noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.entropyFluxDensity F t pos)
+
+/-- Energy flow out of volume -/
+noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.energyFluxDensity F t pos)
+
+end IdealFluid

PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean

@@ -0,0 +1,57 @@
+/-
+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 PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.FluidMechanics.IdealFluid.Euler
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.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 :=
+      ∀ (t : Time) (pos : Space),
+      ∂ₜ (fun t' => F.velocity t' pos) t = (0 : EuclideanSpace ℝ (Fin 3))
+
+/-- Determines whether a flow is isentropic -/
+def IdealFluid.isIsentropic (F: IdealFluid):
+    Prop :=
+      ∀ (t: Time) (pos: Space),
+      ∂ₜ (fun t' => F.entropy t' pos) t = (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 signs
+
+/-- 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 (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0 :=
+      by
+        sorry

PhysLean/FluidMechanics/IdealFluid/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 PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.SpaceAndTime.Time.Derivatives
+public import PhysLean.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),
+      ∂ₜ (fun t' => F.density t' pos) t +
+      Space.div (fun pos' => F.massFluxDensity t pos') pos = (0 : ℝ)
+
+/-- Criterion for incompressibility -/
+public def IdealFluid.isIncompressible (F : IdealFluid):
+    Prop :=
+      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.density t' 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 (fun pos' => F.density t pos') pos = 0) :
+    ∀ (t : Time) (pos : Space), Space.div (fun pos' => F.velocity t pos') pos = 0 := by
+      sorry

PhysLean/FluidMechanics/IdealFluid/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 PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.SpaceAndTime.Time.Derivatives
+public import PhysLean.SpaceAndTime.Space.Derivatives.Grad
+public import PhysLean.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
+        ∂ₜ (fun t'=> F.velocity t' pos) t +
+        (fun i => ⟪v, Space.grad (fun pos' => F.velocity t pos' i) pos⟫_ℝ)
+        = -(1/F.density t pos) • Space.grad (fun pos' => F.pressure t pos') pos + Space.grad g pos