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 01/11] 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 02/11] 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 03/11] 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 04/11] 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

From 75daca2847378ac490e2eb86c6698ac4a53fca51 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 9 Mar 2026 15:28:09 +0000
Subject: [PATCH 05/11] hope for linters finally and continuity

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 36 +++++++++----------
 .../FluidMechanics/IdealFluid/Bernoulli.lean  |  6 ++--
 .../FluidMechanics/IdealFluid/Continuity.lean |  4 +--
 PhysLean/FluidMechanics/IdealFluid/Euler.lean | 16 +++++++++
 4 files changed, 39 insertions(+), 23 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 9fc4840a0..75c1cf630 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -16,22 +16,22 @@ and basic physical properties, meant to be later used for proofs.
 
 open scoped InnerProductSpace
 
-/- Introducing the structure of Ideal Fluids -/
+/-- Introducing the structure of Ideal Fluids -/
 structure IdealFluid where
-  /- The density at a specific point and time -/
+  /-- The density at a specific point and time -/
   density: Time → Space → ℝ
-  /- The velocity at a specific point and time -/
+  /-- The velocity at a specific point and time -/
   velocity: Time → Space → EuclideanSpace ℝ (Fin 3)
-  /- The pressure at a specific point and time -/
+  /-- The pressure at a specific point and time -/
   pressure: Time → Space → ℝ
-  /- The entropy at a specific point and time -/
+  /-- The entropy at a specific point and time -/
   entropy: Time → Space → ℝ
-  /- The enthlapy at a specific point and time -/
+  /-- 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)
@@ -42,17 +42,17 @@ structure IdealFluid where
 namespace IdealFluid
 open MeasureTheory
 
-/- Mass flux density j=ρv -/
+/-- 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 -/
+/-- 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) -/
+/-- 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
@@ -62,31 +62,31 @@ noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 
       scalar • v
 
-/- Volume to introduce surface integrals -/
+/-- Volume to introduce surface integrals -/
 structure FluidVolume where
-  /- The 3D region -/
+  /-- The 3D region -/
   region: Set Space
-  /- The normal pointing outwards -/
+  /-- The normal pointing outwards -/
   normal: Space → EuclideanSpace ℝ (Fin 3)
-  /- 2D measure of the boundary -/
+  /-- 2D measure of the boundary -/
   surfaceMeasure: Measure Space
 
-/- Surface integral of a vector field -/
+/-- 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 -/
+/-- 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 -/
+/-- 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 -/
+/-- 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 a9245b215..80dc877e2 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -7,7 +7,7 @@ Authors: Michał Mogielnicki
 import PhysLean.FluidMechanics.IdealFluid.Basic
 import PhysLean.Mathematics.Calculus.Divergence
 
-/-
+/-!
 This module introduces:
 steady flow,
 ... (still under construction)
@@ -19,12 +19,12 @@ open Space
 
 namespace IdealFluid
 
-/- Determines whether a flow is steady -/
+/-- 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 -/
+/-- Determines whether a flow is isentropic -/
 def isIsentropic (F: IdealFluid):
     Prop :=
       ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => IdealFluid.entropy F t' pos) t = 0
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 9f41a2f9e..8b3bf666f 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -7,7 +7,7 @@ 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.
 -/
@@ -18,7 +18,7 @@ open Space
 
 namespace IdealFluid
 
-/- defining satisfying the equation of continuity -/
+/-- defining satisfying the equation of continuity -/
 def satisfiesContinuity (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space),
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 3901414b5..25ae92c36 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -3,3 +3,19 @@ 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 Euler's equation.
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+namespace IdealFluid
+
+--TODO: Introduce
+end IdealFluid

From 834062ecca9d45ec0e6b3bfb5430ac5437cc0c40 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 9 Mar 2026 16:17:17 +0000
Subject: [PATCH 06/11] fixed imports eaten by changes

---
 PhysLean.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/PhysLean.lean b/PhysLean.lean
index 59e125dd1..210da9550 100644
--- a/PhysLean.lean
+++ b/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

From 1df9a86a72cfe4cf2011dc5cacb6bfa575869ea3 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Tue, 17 Mar 2026 09:37:25 +0000
Subject: [PATCH 07/11] Build working

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 16 +++++++++-------
 .../FluidMechanics/IdealFluid/Bernoulli.lean  | 19 +++++++++----------
 .../FluidMechanics/IdealFluid/Continuity.lean | 18 +++++++++---------
 PhysLean/FluidMechanics/IdealFluid/Euler.lean |  9 +++++++--
 4 files changed, 34 insertions(+), 28 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 75c1cf630..ef4626745 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -4,10 +4,12 @@ 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
+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
@@ -17,7 +19,7 @@ and basic physical properties, meant to be later used for proofs.
 open scoped InnerProductSpace
 
 /-- Introducing the structure of Ideal Fluids -/
-structure IdealFluid where
+public structure IdealFluid where
   /-- The density at a specific point and time -/
   density: Time → Space → ℝ
   /-- The velocity at a specific point and time -/
@@ -43,12 +45,12 @@ namespace IdealFluid
 open MeasureTheory
 
 /-- Mass flux density j=ρv -/
-def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public 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):
+public 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)
 
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 80dc877e2..8ded3bcdc 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -4,8 +4,11 @@ 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
+module
+
+public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.SpaceAndTime.Time.Derivatives
 
 /-!
 This module introduces:
@@ -17,18 +20,14 @@ open scoped InnerProductSpace
 open Time
 open Space
 
-namespace IdealFluid
-
 /-- Determines whether a flow is steady -/
-def isSteady (F: IdealFluid) :
+def IdealFluid.isSteady (F: IdealFluid) :
     Prop :=
-      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => IdealFluid.velocity F t' pos) t = 0
+      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.velocity t' pos) t = (0 : EuclideanSpace ℝ (Fin 3))
 
 /-- Determines whether a flow is isentropic -/
-def isIsentropic (F: IdealFluid):
+def IdealFluid.isIsentropic (F: IdealFluid):
     Prop :=
-      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => IdealFluid.entropy F t' pos) t = 0
+      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => F.entropy 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 8b3bf666f..09ca420d4 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -4,8 +4,12 @@ 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
+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.
@@ -16,17 +20,13 @@ open scoped InnerProductSpace
 open Time
 open Space
 
-namespace IdealFluid
-
 /-- defining satisfying the equation of continuity -/
-def satisfiesContinuity (F : IdealFluid):
+def IdealFluid.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
+      ∂ₜ (fun t' => F.density t' pos) t +
+      Space.div (fun pos' => F.massFluxDensity t pos') pos = (0 : ℝ)
 
 
 -- TODO: Add lemmas for continuity with different models.
 -- TODO: Add definition and lemmas for Incompressibility.
-
-end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 25ae92c36..a36fad807 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -4,8 +4,13 @@ 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
+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.

From 3dc2ff3b6beede98a8abe20c1e89aec3d3bb8df1 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Tue, 17 Mar 2026 13:10:43 +0000
Subject: [PATCH 08/11] hope

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean |  8 +++---
 .../FluidMechanics/IdealFluid/Bernoulli.lean  | 26 ++++++++++++++++---
 .../FluidMechanics/IdealFluid/Continuity.lean |  6 +----
 PhysLean/FluidMechanics/IdealFluid/Euler.lean | 12 ++++++---
 4 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index ef4626745..237fb8c39 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -28,8 +28,8 @@ public structure IdealFluid where
   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 → ℝ
+  /-- The enthalpy at a specific point and time -/
+  enthalpy: Time → Space → ℝ
 
   density_pos: ∀ t pos, 0 < density t pos
 
@@ -39,7 +39,7 @@ public structure IdealFluid where
   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)
+  enthalpy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthalpy s.1 s.2)
 
 namespace IdealFluid
 open MeasureTheory
@@ -57,7 +57,7 @@ public def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 /-- 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
+      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)
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 8ded3bcdc..a7af2e56a 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -7,6 +7,7 @@ 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
 
@@ -23,11 +24,30 @@ 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))
+      ∀ (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 : ℝ)
+      ∀ (t: Time) (pos: Space),
+      ∂ₜ (fun t' => F.entropy t' pos) t = (0 : ℝ)
 
--- TODO: Provide the Bernoulli's equation (after fun derivatoins)
+/-- 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
+
+/-- Derivation:
+  If the flow is steady and isentropic, the bernoulli equation is constant
+-/
+theorem bernoulli_derivation (F: IdealFluid) (Eul: F.satisfiesEuler g) (Stdy: F.isSteady)
+(Istrpc: F.isIsentropic) (g: Space → ℝ) (t: Time) (pos: Space):
+    let v := F.velocity t pos
+    ⟪v, Space.grad (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0
+    := by
+      sorry
+
+--TODO: Complete the proofs
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 09ca420d4..12d037948 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -21,12 +21,8 @@ open Time
 open Space
 
 /-- defining satisfying the equation of continuity -/
-def IdealFluid.satisfiesContinuity (F : IdealFluid):
+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 : ℝ)
-
-
--- TODO: Add lemmas for continuity with different models.
--- TODO: Add definition and lemmas for Incompressibility.
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index a36fad807..872182dea 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -20,7 +20,11 @@ open scoped InnerProductSpace
 open Time
 open Space
 
-namespace IdealFluid
-
---TODO: Introduce
-end IdealFluid
+/-- 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

From d175f46fbc3c497af0e65b0c4eeb82c90a09f5fb Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Wed, 18 Mar 2026 20:11:37 +0000
Subject: [PATCH 09/11] smol changes

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean      |  8 ++++----
 PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean  | 14 +++++++-------
 PhysLean/FluidMechanics/IdealFluid/Continuity.lean |  5 +++++
 3 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 237fb8c39..1879030f3 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -45,17 +45,17 @@ namespace IdealFluid
 open MeasureTheory
 
 /-- Mass flux density j=ρv -/
-public def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public abbrev massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
-     (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+      F.density t pos • F.velocity t pos
 
 /-- Entropy flux density ρsv -/
-public def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+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 def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+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
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index a7af2e56a..b2329d75d 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -43,11 +43,11 @@ noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
 /-- Derivation:
   If the flow is steady and isentropic, the bernoulli equation is constant
 -/
-theorem bernoulli_derivation (F: IdealFluid) (Eul: F.satisfiesEuler g) (Stdy: F.isSteady)
-(Istrpc: F.isIsentropic) (g: Space → ℝ) (t: Time) (pos: Space):
+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
-
---TODO: Complete the proofs
+    ⟪v, Space.grad (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0 :=
+      by
+        sorry
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 12d037948..826bf01c7 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -26,3 +26,8 @@ public def IdealFluid.satisfiesContinuity (F : IdealFluid):
       ∀ (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

From ad5f26ce4640fedad916eb5a043579420cf58530 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Wed, 18 Mar 2026 20:16:18 +0000
Subject: [PATCH 10/11] a sorryful theorem

---
 PhysLean/FluidMechanics/IdealFluid/Continuity.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 826bf01c7..ecea01b9f 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -31,3 +31,12 @@ public def IdealFluid.satisfiesContinuity (F : IdealFluid):
 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

From d020adb1bde6d08f07caa209cf280bad4b3ecd51 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Thu, 19 Mar 2026 12:51:19 +0000
Subject: [PATCH 11/11] suggestions for myself

---
 PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean  | 4 ++++
 PhysLean/FluidMechanics/IdealFluid/Continuity.lean | 1 -
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index b2329d75d..451de1836 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -33,6 +33,8 @@ def IdealFluid.isIsentropic (F: IdealFluid):
       ∀ (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 → ℝ):
@@ -40,6 +42,8 @@ noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
       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
 -/
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index ecea01b9f..f537b01fd 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -32,7 +32,6 @@ 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)