From 4e5b54855346abf494f4b187bc092a867c43028a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 1 Apr 2026 19:22:40 +0100 Subject: [PATCH] feat: Move variational calculus --- PhysLean.lean | 12 ++++++------ PhysLean/ClassicalMechanics/EulerLagrange.lean | 2 +- PhysLean/ClassicalMechanics/HamiltonsEquations.lean | 2 +- .../Lagrangian/TotalDerivativeEquivalence.lean | 2 +- .../VariationalCalculus/Basic.lean | 2 +- .../VariationalCalculus/HasVarAdjDeriv.lean | 2 +- .../VariationalCalculus/HasVarAdjoint.lean | 2 +- .../VariationalCalculus/HasVarGradient.lean | 2 +- .../IsLocalizedfunctionTransform.lean | 2 +- .../VariationalCalculus/IsTestFunction.lean | 0 .../Electromagnetism/Kinematics/EMPotential.lean | 2 +- 11 files changed, 15 insertions(+), 15 deletions(-) rename PhysLean/{Mathematics => ClassicalMechanics}/VariationalCalculus/Basic.lean (99%) rename PhysLean/{Mathematics => ClassicalMechanics}/VariationalCalculus/HasVarAdjDeriv.lean (99%) rename PhysLean/{Mathematics => ClassicalMechanics}/VariationalCalculus/HasVarAdjoint.lean (99%) rename PhysLean/{Mathematics => ClassicalMechanics}/VariationalCalculus/HasVarGradient.lean (98%) rename PhysLean/{Mathematics => ClassicalMechanics}/VariationalCalculus/IsLocalizedfunctionTransform.lean (99%) rename PhysLean/{Mathematics => ClassicalMechanics}/VariationalCalculus/IsTestFunction.lean (100%) 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