From 347df8fa66985bd575c7e516db8540a77eaed181 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 16 Feb 2026 10:19:00 +0000
Subject: [PATCH 1/4] Initial IdealFluid structure

---
 PhysLean/FluidMechanics/Basic.lean            | 23 +++++++++++++++++++
 .../FluidMechanics/IdealFluid/Bernoulli.lean  |  5 ++++
 .../FluidMechanics/IdealFluid/Continuity.lean |  5 ++++
 PhysLean/FluidMechanics/IdealFluid/Euler.lean |  8 +++++++
 4 files changed, 41 insertions(+)
 create mode 100644 PhysLean/FluidMechanics/Basic.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Continuity.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Euler.lean

diff --git a/PhysLean/FluidMechanics/Basic.lean b/PhysLean/FluidMechanics/Basic.lean
new file mode 100644
index 000000000..3b4cc332c
--- /dev/null
+++ b/PhysLean/FluidMechanics/Basic.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+import PhysLean.SpaceAndTime.Space.Basic
+import PhysLean.SpaceAndTime.Time.Basic
+/-!
+This module introduces the idea of an ideal fluid and the mass flux density. The rest of the early workings is to be seen in ./IdealFluid/
+-/
+open scoped InnerProductSpace
+
+structure IdealFluid where
+  density: Time → Space → ℝ
+  velocity: Time → Space→ Space
+  pressure: Time → Space → ℝ
+
+namespace IdealFluid
+
+def massFluxDensity (F: IdealFluid) (t : Time) (pos : Space ) :
+    Space := (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+
+end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
new file mode 100644
index 000000000..3901414b5
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -0,0 +1,5 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
new file mode 100644
index 000000000..3901414b5
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -0,0 +1,5 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
new file mode 100644
index 000000000..7d1d49546
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+/-!
+This module introduces Euler's equation
+-/

From 503a3eefd1d8ba0812da763042d2436ac651cd24 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 23 Feb 2026 14:08:06 +0000
Subject: [PATCH 2/4] Added definitions and fixed the properties of earlier
 defined IdealFluid

---
 PhysLean/FluidMechanics/Basic.lean            | 23 -------
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 63 +++++++++++++++++++
 PhysLean/FluidMechanics/IdealFluid/Euler.lean |  3 -
 3 files changed, 63 insertions(+), 26 deletions(-)
 delete mode 100644 PhysLean/FluidMechanics/Basic.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Basic.lean

diff --git a/PhysLean/FluidMechanics/Basic.lean b/PhysLean/FluidMechanics/Basic.lean
deleted file mode 100644
index 3b4cc332c..000000000
--- a/PhysLean/FluidMechanics/Basic.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michał Mogielnicki
--/
-import PhysLean.SpaceAndTime.Space.Basic
-import PhysLean.SpaceAndTime.Time.Basic
-/-!
-This module introduces the idea of an ideal fluid and the mass flux density. The rest of the early workings is to be seen in ./IdealFluid/
--/
-open scoped InnerProductSpace
-
-structure IdealFluid where
-  density: Time → Space → ℝ
-  velocity: Time → Space→ Space
-  pressure: Time → Space → ℝ
-
-namespace IdealFluid
-
-def massFluxDensity (F: IdealFluid) (t : Time) (pos : Space ) :
-    Space := (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
-
-end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
new file mode 100644
index 000000000..15dd0d9d9
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import PhysLean.SpaceAndTime.Space.Basic
+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
+
+structure IdealFluid where
+  density: Time → Space → ℝ
+  velocity: Time → Space → EuclideanSpace ℝ (Fin 3)
+  pressure: Time → Space → ℝ
+
+  entropy: Time → Space → ℝ
+  enthlapy: 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)
+  enthlapy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthlapy s.1 s.2)
+
+namespace IdealFluid
+
+/-!
+Here lays defined:
+  the mass flux density
+  entropy flux density
+  energy flux density
+  flow out of a volume
+-/
+
+def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+     (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+
+def 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)
+
+noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+      let w := IdealFluid.enthlapy 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
+
+/-Still a need to introduce flow out of volume-/
+
+end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 7d1d49546..3901414b5 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -3,6 +3,3 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
-/-!
-This module introduces Euler's equation
--/

From 818fd23ff19916f5bec77fcecb0ac79a939040de Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Tue, 24 Feb 2026 10:16:02 +0000
Subject: [PATCH 3/4] Imported to PhysLean.lean and added the flow out of the
 volume

---
 PhysLean.lean                                 |  4 +++
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 31 ++++++++++++++++---
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/PhysLean.lean b/PhysLean.lean
index 283c464e5..160955282 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -41,6 +41,10 @@ import PhysLean.Electromagnetism.PointParticle.ThreeDimension
 import PhysLean.Electromagnetism.Vacuum.Constant
 import PhysLean.Electromagnetism.Vacuum.HarmonicWave
 import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.FluidMechanics.IdealFluid.Bernoulli
+import PhysLean.FluidMechanics.IdealFluid.Continuity
+import PhysLean.FluidMechanics.IdealFluid.Euler
 import PhysLean.Mathematics.Calculus.AdjFDeriv
 import PhysLean.Mathematics.Calculus.Divergence
 import PhysLean.Mathematics.DataStructures.FourTree.Basic
diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 15dd0d9d9..cd57cb894 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -21,7 +21,7 @@ structure IdealFluid where
   entropy: Time → Space → ℝ
   enthlapy: Time → Space → ℝ
 
-  density_pos: ∀ t, pos 0 < density t pos
+  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)
@@ -32,13 +32,12 @@ structure IdealFluid where
   enthlapy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthlapy s.1 s.2)
 
 namespace IdealFluid
-
+open MeasureTheory
 /-!
 Here lays defined:
   the mass flux density
   entropy flux density
   energy flux density
-  flow out of a volume
 -/
 
 def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
@@ -58,6 +57,30 @@ noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 
       scalar • v
 
-/-Still a need to introduce flow out of volume-/
+/-I hereby describe the:
+FluidVolume structure
+surface integral
+flow out of volume-/
+
+structure FluidVolume where
+  region: Set Space
+  normal: Space → EuclideanSpace ℝ (Fin 3)
+  surfaceMeasure: Measure Space
+
+noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpace ℝ (Fin 3)):
+    ℝ :=
+      ∫ (pos: Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
+
+noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.massFluxDensity F t pos)
+
+noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.entropyFluxDensity F t pos)
+
+noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.energyFluxDensity F t pos)
 
 end IdealFluid

From 53e4dc1c4d985310d53aeb0867be66b59aa98b3e Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Thu, 26 Feb 2026 14:45:41 +0000
Subject: [PATCH 4/4] pls linters (oh and continuity, isentropy and steadiness)

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 34 ++++++++++++-------
 .../FluidMechanics/IdealFluid/Bernoulli.lean  | 29 ++++++++++++++++
 .../FluidMechanics/IdealFluid/Continuity.lean | 27 +++++++++++++++
 3 files changed, 77 insertions(+), 13 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index cd57cb894..9fc4840a0 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -3,27 +3,35 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import PhysLean.SpaceAndTime.Space.Basic
 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 -/
 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 enthlapy at a specific point and time -/
   enthlapy: Time → Space → ℝ
 
   density_pos: ∀ t pos, 0 < density t pos
 
-  /-- Ensuring that all are differentiable for more complex equations. -/
+  /- 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)
@@ -33,21 +41,18 @@ structure IdealFluid where
 
 namespace IdealFluid
 open MeasureTheory
-/-!
-Here lays defined:
-  the mass flux density
-  entropy flux density
-  energy flux density
--/
 
+/- Mass flux density j=ρv -/
 def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
      (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
+/- Entropy flux density ρsv -/
 def 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 def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       let w := IdealFluid.enthlapy F t pos
@@ -57,28 +62,31 @@ noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 
       scalar • v
 
-/-I hereby describe the:
-FluidVolume structure
-surface integral
-flow out of volume-/
-
+/- 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)
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 3901414b5..a9245b215 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -3,3 +3,32 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.Mathematics.Calculus.Divergence
+
+/-
+This module introduces:
+steady flow,
+... (still under construction)
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+namespace IdealFluid
+
+/- Determines whether a flow is steady -/
+def isSteady (F: IdealFluid) :
+    Prop :=
+      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => IdealFluid.velocity F t' pos) t = 0
+
+/- Determines whether a flow is isentropic -/
+def isIsentropic (F: IdealFluid):
+    Prop :=
+      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => IdealFluid.entropy F t' pos) t = 0
+
+-- TODO: Provide the Bernoulli's equation (after fun derivatoins)
+
+end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 3901414b5..9f41a2f9e 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -3,3 +3,30 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.Mathematics.Calculus.Divergence
+
+/-
+This module introduces the continuity criterium.
+There is potential to add various different lemmas expanding on this.
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+namespace IdealFluid
+
+/- defining satisfying the equation of continuity -/
+def satisfiesContinuity (F : IdealFluid):
+    Prop :=
+      ∀ (t : Time) (pos : Space),
+      ∂ₜ (fun t' => IdealFluid.density F t' pos) t +
+      Space.div (fun pos' => IdealFluid.massFluxDensity F t pos') pos = 0
+
+
+-- TODO: Add lemmas for continuity with different models.
+-- TODO: Add definition and lemmas for Incompressibility.
+
+end IdealFluid