Skip to content

feat: Move variational calculus #1018

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

Open
jstoobysmith wants to merge 1 commit into
base: master
Choose a base branch
from
Open

feat: Move variational calculus #1018

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
12 changes: 6 additions & 6 deletions PhysLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,12 @@ public import PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum
public import PhysLean.ClassicalMechanics.RigidBody.Basic
public import PhysLean.ClassicalMechanics.RigidBody.SolidSphere
public import PhysLean.ClassicalMechanics.Scattering.RigidSphere
public import PhysLean.ClassicalMechanics.VariationalCalculus.Basic
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarAdjDeriv
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarAdjoint
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarGradient
public import PhysLean.ClassicalMechanics.VariationalCalculus.IsLocalizedfunctionTransform
public import PhysLean.ClassicalMechanics.VariationalCalculus.IsTestFunction
public import PhysLean.ClassicalMechanics.Vibrations.LinearTriatomic
public import PhysLean.ClassicalMechanics.WaveEquation.Basic
public import PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
Expand Down Expand Up @@ -73,12 +79,6 @@ public import PhysLean.Mathematics.SO3.Basic
public import PhysLean.Mathematics.SchurTriangulation
public import PhysLean.Mathematics.SpecialFunctions.PhysHermite
public import PhysLean.Mathematics.Trigonometry.Tanh
public import PhysLean.Mathematics.VariationalCalculus.Basic
public import PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
public import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
public import PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
public import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
public import PhysLean.Meta.AllFilePaths
public import PhysLean.Meta.Basic
public import PhysLean.Meta.Informal.Basic
Expand Down
2 changes: 1 addition & 1 deletion PhysLean/ClassicalMechanics/EulerLagrange.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarGradient
/-!
# Euler-Lagrange equations
Expand Down
2 changes: 1 addition & 1 deletion PhysLean/ClassicalMechanics/HamiltonsEquations.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarGradient
/-!
# Hamilton's equations
Expand Down
2 changes: 1 addition & 1 deletion PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Rein Zustand
-/
module

public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarGradient
/-!
# Equivalent Lagrangians under Total Derivatives
Expand Down
2 changes: 1 addition & 1 deletion ...athematics/VariationalCalculus/Basic.lean → ...lMechanics/VariationalCalculus/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
public import PhysLean.ClassicalMechanics.VariationalCalculus.IsTestFunction
/-!
# Fundamental lemma of the calculus of variations
Expand Down
2 changes: 1 addition & 1 deletion ...s/VariationalCalculus/HasVarAdjDeriv.lean → ...s/VariationalCalculus/HasVarAdjDeriv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarAdjoint
/-!
# Variational adjoint derivative
Expand Down
2 changes: 1 addition & 1 deletion ...cs/VariationalCalculus/HasVarAdjoint.lean → ...cs/VariationalCalculus/HasVarAdjoint.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
public import PhysLean.ClassicalMechanics.VariationalCalculus.IsLocalizedfunctionTransform
/-!
# Variational adjoint
Expand Down
2 changes: 1 addition & 1 deletion ...s/VariationalCalculus/HasVarGradient.lean → ...s/VariationalCalculus/HasVarGradient.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarAdjDeriv
/-!
# Variational gradient
Expand Down
2 changes: 1 addition & 1 deletion ...alculus/IsLocalizedfunctionTransform.lean → ...alculus/IsLocalizedfunctionTransform.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import PhysLean.Mathematics.VariationalCalculus.Basic
public import PhysLean.ClassicalMechanics.VariationalCalculus.Basic
/-!
# Localized function transforms
Expand Down
0 ...s/VariationalCalculus/IsTestFunction.lean → ...s/VariationalCalculus/IsTestFunction.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion PhysLean/Electromagnetism/Kinematics/EMPotential.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module

public import PhysLean.Electromagnetism.Basic
public import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
public import PhysLean.ClassicalMechanics.VariationalCalculus.HasVarGradient
/-!
# The Electromagnetic Potential
Expand Down
Loading