diff --git a/PhysLean.lean b/PhysLean.lean index 8c7c7dcb2..523f36d6b 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -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 @@ -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 diff --git a/PhysLean/ClassicalMechanics/EulerLagrange.lean b/PhysLean/ClassicalMechanics/EulerLagrange.lean index c81837a69..0289b0d1a 100644 --- a/PhysLean/ClassicalMechanics/EulerLagrange.lean +++ b/PhysLean/ClassicalMechanics/EulerLagrange.lean @@ -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 diff --git a/PhysLean/ClassicalMechanics/HamiltonsEquations.lean b/PhysLean/ClassicalMechanics/HamiltonsEquations.lean index e43db2339..b2953b8d5 100644 --- a/PhysLean/ClassicalMechanics/HamiltonsEquations.lean +++ b/PhysLean/ClassicalMechanics/HamiltonsEquations.lean @@ -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 diff --git a/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean b/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean index 9d60d665c..d566447ee 100644 --- a/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean +++ b/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean @@ -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 diff --git a/PhysLean/Mathematics/VariationalCalculus/Basic.lean b/PhysLean/ClassicalMechanics/VariationalCalculus/Basic.lean similarity index 99% rename from PhysLean/Mathematics/VariationalCalculus/Basic.lean rename to PhysLean/ClassicalMechanics/VariationalCalculus/Basic.lean index 3061532bc..1fd5b4f38 100644 --- a/PhysLean/Mathematics/VariationalCalculus/Basic.lean +++ b/PhysLean/ClassicalMechanics/VariationalCalculus/Basic.lean @@ -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 diff --git a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean b/PhysLean/ClassicalMechanics/VariationalCalculus/HasVarAdjDeriv.lean similarity index 99% rename from PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean rename to PhysLean/ClassicalMechanics/VariationalCalculus/HasVarAdjDeriv.lean index c62ad81f1..4553f9e47 100644 --- a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean +++ b/PhysLean/ClassicalMechanics/VariationalCalculus/HasVarAdjDeriv.lean @@ -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 diff --git a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean b/PhysLean/ClassicalMechanics/VariationalCalculus/HasVarAdjoint.lean similarity index 99% rename from PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean rename to PhysLean/ClassicalMechanics/VariationalCalculus/HasVarAdjoint.lean index 19f86fa1b..b26c525ee 100644 --- a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean +++ b/PhysLean/ClassicalMechanics/VariationalCalculus/HasVarAdjoint.lean @@ -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 diff --git a/PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean b/PhysLean/ClassicalMechanics/VariationalCalculus/HasVarGradient.lean similarity index 98% rename from PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean rename to PhysLean/ClassicalMechanics/VariationalCalculus/HasVarGradient.lean index b9dfa00bc..a2ab70bc4 100644 --- a/PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean +++ b/PhysLean/ClassicalMechanics/VariationalCalculus/HasVarGradient.lean @@ -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 diff --git a/PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean b/PhysLean/ClassicalMechanics/VariationalCalculus/IsLocalizedfunctionTransform.lean similarity index 99% rename from PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean rename to PhysLean/ClassicalMechanics/VariationalCalculus/IsLocalizedfunctionTransform.lean index 479fa55c9..2d6b77eb4 100644 --- a/PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean +++ b/PhysLean/ClassicalMechanics/VariationalCalculus/IsLocalizedfunctionTransform.lean @@ -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 diff --git a/PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean b/PhysLean/ClassicalMechanics/VariationalCalculus/IsTestFunction.lean similarity index 100% rename from PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean rename to PhysLean/ClassicalMechanics/VariationalCalculus/IsTestFunction.lean diff --git a/PhysLean/Electromagnetism/Kinematics/EMPotential.lean b/PhysLean/Electromagnetism/Kinematics/EMPotential.lean index be3dd86cf..e8c7ea5c6 100644 --- a/PhysLean/Electromagnetism/Kinematics/EMPotential.lean +++ b/PhysLean/Electromagnetism/Kinematics/EMPotential.lean @@ -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