Skip to content

Initial IdealFluid structure #949

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
mog1el wants to merge 14 commits into
base: master
Choose a base branch
from
+235 −0
Draft

Initial IdealFluid structure #949

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
347df8f
Initial IdealFluid structure
mog1el Feb 16, 2026
503a3ee
Added definitions and fixed the properties of earlier defined IdealFluid
mog1el Feb 23, 2026
818fd23
Imported to PhysLean.lean and added the flow out of the volume
mog1el Feb 24, 2026
53e4dc1
pls linters (oh and continuity, isentropy and steadiness)
mog1el Feb 26, 2026
75daca2
hope for linters finally and continuity
mog1el Mar 9, 2026
8e2fec1
Merge branch 'master' into Fluids
mog1el Mar 9, 2026
834062e
fixed imports eaten by changes
mog1el Mar 9, 2026
1df9a86
Build working
mog1el Mar 17, 2026
3dc2ff3
hope
mog1el Mar 17, 2026
d175f46
smol changes
mog1el Mar 18, 2026
ad5f26c
a sorryful theorem
mog1el Mar 18, 2026
d020adb
suggestions for myself
mog1el Mar 19, 2026
49a8720
Mderiv and fun
mog1el Apr 29, 2026
d911fb3
back (material, fun)
mog1el Apr 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 23 additions & 0 deletions PhysLean/FluidMechanics/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
-/
Comment thread
mog1el marked this conversation as resolved.
Outdated
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
Comment thread
mog1el marked this conversation as resolved.
Outdated
pressure: Time → Space → ℝ
Comment thread
mog1el marked this conversation as resolved.
Outdated

namespace IdealFluid

def massFluxDensity (F: IdealFluid) (t : Time) (pos : Space ) :
Space := (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)

end IdealFluid
5 changes: 5 additions & 0 deletions PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
-/
5 changes: 5 additions & 0 deletions PhysLean/FluidMechanics/IdealFluid/Continuity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
-/
8 changes: 8 additions & 0 deletions PhysLean/FluidMechanics/IdealFluid/Euler.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
-/
Loading