diff --git a/PhysLean.lean b/PhysLean.lean
index 2d8e75697..59e125dd1 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -1,406 +1,408 @@
-import PhysLean.ClassicalMechanics.Basic
-import PhysLean.ClassicalMechanics.DampedHarmonicOscillator.Basic
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
-import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
-import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
-import PhysLean.ClassicalMechanics.HarmonicOscillator.Solution
-import PhysLean.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence
-import PhysLean.ClassicalMechanics.Mass.MassUnit
-import PhysLean.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
-import PhysLean.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
-import PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum
-import PhysLean.ClassicalMechanics.RigidBody.Basic
-import PhysLean.ClassicalMechanics.RigidBody.SolidSphere
-import PhysLean.ClassicalMechanics.Scattering.RigidSphere
-import PhysLean.ClassicalMechanics.Vibrations.LinearTriatomic
-import PhysLean.ClassicalMechanics.WaveEquation.Basic
-import PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
-import PhysLean.CondensedMatter.Basic
-import PhysLean.CondensedMatter.TightBindingChain.Basic
-import PhysLean.Cosmology.Basic
-import PhysLean.Cosmology.FLRW.Basic
-import PhysLean.Electromagnetism.Basic
-import PhysLean.Electromagnetism.Charge.ChargeUnit
-import PhysLean.Electromagnetism.Current.CircularCoil
-import PhysLean.Electromagnetism.Current.InfiniteWire
-import PhysLean.Electromagnetism.Dynamics.Basic
-import PhysLean.Electromagnetism.Dynamics.CurrentDensity
-import PhysLean.Electromagnetism.Dynamics.Hamiltonian
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
-import PhysLean.Electromagnetism.Dynamics.KineticTerm
-import PhysLean.Electromagnetism.Dynamics.Lagrangian
-import PhysLean.Electromagnetism.Kinematics.Boosts
-import PhysLean.Electromagnetism.Kinematics.EMPotential
-import PhysLean.Electromagnetism.Kinematics.ElectricField
-import PhysLean.Electromagnetism.Kinematics.FieldStrength
-import PhysLean.Electromagnetism.Kinematics.MagneticField
-import PhysLean.Electromagnetism.Kinematics.ScalarPotential
-import PhysLean.Electromagnetism.Kinematics.VectorPotential
-import PhysLean.Electromagnetism.PointParticle.OneDimension
-import PhysLean.Electromagnetism.PointParticle.ThreeDimension
-import PhysLean.Electromagnetism.Vacuum.Constant
-import PhysLean.Electromagnetism.Vacuum.HarmonicWave
-import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
-import PhysLean.Mathematics.Calculus.AdjFDeriv
-import PhysLean.Mathematics.Calculus.Divergence
-import PhysLean.Mathematics.DataStructures.FourTree.Basic
-import PhysLean.Mathematics.DataStructures.FourTree.UniqueMap
-import PhysLean.Mathematics.DataStructures.Matrix.LieTrace
-import PhysLean.Mathematics.Distribution.Basic
-import PhysLean.Mathematics.Distribution.PowMul
-import PhysLean.Mathematics.FDerivCurry
-import PhysLean.Mathematics.Fin
-import PhysLean.Mathematics.Fin.Involutions
-import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
-import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
-import PhysLean.Mathematics.InnerProductSpace.Adjoint
-import PhysLean.Mathematics.InnerProductSpace.Basic
-import PhysLean.Mathematics.InnerProductSpace.Calculus
-import PhysLean.Mathematics.InnerProductSpace.Submodule
-import PhysLean.Mathematics.KroneckerDelta
-import PhysLean.Mathematics.LinearMaps
-import PhysLean.Mathematics.List
-import PhysLean.Mathematics.List.InsertIdx
-import PhysLean.Mathematics.List.InsertionSort
-import PhysLean.Mathematics.PiTensorProduct
-import PhysLean.Mathematics.RatComplexNum
-import PhysLean.Mathematics.SO3.Basic
-import PhysLean.Mathematics.SchurTriangulation
-import PhysLean.Mathematics.SpecialFunctions.PhysHermite
-import PhysLean.Mathematics.Trigonometry.Tanh
-import PhysLean.Mathematics.VariationalCalculus.Basic
-import PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
-import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
-import PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
-import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
-import PhysLean.Meta.AllFilePaths
-import PhysLean.Meta.Basic
-import PhysLean.Meta.Informal.Basic
-import PhysLean.Meta.Informal.Post
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.Meta.Linters.Sorry
-import PhysLean.Meta.Notes.Basic
-import PhysLean.Meta.Notes.HTMLNote
-import PhysLean.Meta.Notes.NoteFile
-import PhysLean.Meta.Notes.ToHTML
-import PhysLean.Meta.Remark.Basic
-import PhysLean.Meta.Remark.Properties
-import PhysLean.Meta.Sorry
-import PhysLean.Meta.TODO.Basic
-import PhysLean.Meta.TransverseTactics
-import PhysLean.Optics.Basic
-import PhysLean.Optics.Polarization.Basic
-import PhysLean.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
-import PhysLean.Particles.BeyondTheStandardModel.PatiSalam.Basic
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.FamilyMaps
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BoundPlaneDim
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol
-import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
-import PhysLean.Particles.BeyondTheStandardModel.Spin10.Basic
-import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
-import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GramMatrix
-import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Potential
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.Basic
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.Relations
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.Rows
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
-import PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
-import PhysLean.Particles.NeutrinoPhysics.Basic
-import PhysLean.Particles.StandardModel.AnomalyCancellation.Basic
-import PhysLean.Particles.StandardModel.AnomalyCancellation.FamilyMaps
-import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
-import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas
-import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization
-import PhysLean.Particles.StandardModel.AnomalyCancellation.Permutations
-import PhysLean.Particles.StandardModel.Basic
-import PhysLean.Particles.StandardModel.HiggsBoson.Basic
-import PhysLean.Particles.StandardModel.HiggsBoson.Potential
-import PhysLean.Particles.StandardModel.Representations
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.HyperCharge
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations
-import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Map
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimalSuperSet
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.FinsetTerms
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfFieldLabel
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfPotentialTerm
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoClosed
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrained
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa
-import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.ZMod
-import PhysLean.Particles.SuperSymmetry.SU5.FieldLabels
-import PhysLean.Particles.SuperSymmetry.SU5.Potential
-import PhysLean.QFT.AnomalyCancellation.Basic
-import PhysLean.QFT.AnomalyCancellation.GroupActions
-import PhysLean.QFT.PerturbationTheory.CreateAnnihilate
-import PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Basic
-import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic
-import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading
-import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
-import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
-import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
-import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
-import PhysLean.QFT.PerturbationTheory.FieldSpecification.Basic
-import PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp
-import PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnSection
-import PhysLean.QFT.PerturbationTheory.FieldSpecification.Filters
-import PhysLean.QFT.PerturbationTheory.FieldSpecification.NormalOrder
-import PhysLean.QFT.PerturbationTheory.FieldSpecification.TimeOrder
-import PhysLean.QFT.PerturbationTheory.FieldStatistics.Basic
-import PhysLean.QFT.PerturbationTheory.FieldStatistics.ExchangeSign
-import PhysLean.QFT.PerturbationTheory.FieldStatistics.OfFinset
-import PhysLean.QFT.PerturbationTheory.Koszul.KoszulSign
-import PhysLean.QFT.PerturbationTheory.Koszul.KoszulSignInsert
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.Grading
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTerm
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTheorem
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.SuperCommute
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeContraction
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeOrder
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.Universality
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.WickTerm
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
-import PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheoremNormal
-import PhysLean.QFT.PerturbationTheory.WickContraction.Basic
-import PhysLean.QFT.PerturbationTheory.WickContraction.Card
-import PhysLean.QFT.PerturbationTheory.WickContraction.Erase
-import PhysLean.QFT.PerturbationTheory.WickContraction.ExtractEquiv
-import PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContract
-import PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
-import PhysLean.QFT.PerturbationTheory.WickContraction.Involutions
-import PhysLean.QFT.PerturbationTheory.WickContraction.IsFull
-import PhysLean.QFT.PerturbationTheory.WickContraction.Join
-import PhysLean.QFT.PerturbationTheory.WickContraction.Perm
-import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Basic
-import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
-import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
-import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Join
-import PhysLean.QFT.PerturbationTheory.WickContraction.Singleton
-import PhysLean.QFT.PerturbationTheory.WickContraction.StaticContract
-import PhysLean.QFT.PerturbationTheory.WickContraction.SubContraction
-import PhysLean.QFT.PerturbationTheory.WickContraction.TimeCond
-import PhysLean.QFT.PerturbationTheory.WickContraction.TimeContract
-import PhysLean.QFT.PerturbationTheory.WickContraction.Uncontracted
-import PhysLean.QFT.PerturbationTheory.WickContraction.UncontractedList
-import PhysLean.QFT.QED.AnomalyCancellation.Basic
-import PhysLean.QFT.QED.AnomalyCancellation.BasisLinear
-import PhysLean.QFT.QED.AnomalyCancellation.ConstAbs
-import PhysLean.QFT.QED.AnomalyCancellation.Even.BasisLinear
-import PhysLean.QFT.QED.AnomalyCancellation.Even.LineInCubic
-import PhysLean.QFT.QED.AnomalyCancellation.Even.Parameterization
-import PhysLean.QFT.QED.AnomalyCancellation.LineInPlaneCond
-import PhysLean.QFT.QED.AnomalyCancellation.LowDim.One
-import PhysLean.QFT.QED.AnomalyCancellation.LowDim.Three
-import PhysLean.QFT.QED.AnomalyCancellation.LowDim.Two
-import PhysLean.QFT.QED.AnomalyCancellation.Odd.BasisLinear
-import PhysLean.QFT.QED.AnomalyCancellation.Odd.LineInCubic
-import PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
-import PhysLean.QFT.QED.AnomalyCancellation.Permutations
-import PhysLean.QFT.QED.AnomalyCancellation.Sorts
-import PhysLean.QFT.QED.AnomalyCancellation.VectorLike
-import PhysLean.QuantumMechanics.DDimensions.Hydrogen.Basic
-import PhysLean.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVector
-import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
-import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation
-import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
-import PhysLean.QuantumMechanics.DDimensions.Operators.Position
-import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
-import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
-import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
-import PhysLean.QuantumMechanics.FiniteTarget.Basic
-import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
-import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
-import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
-import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
-import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
-import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Examples
-import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
-import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
-import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
-import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PlaneWaves
-import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PositionStates
-import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
-import PhysLean.QuantumMechanics.OneDimension.Operators.Commutation
-import PhysLean.QuantumMechanics.OneDimension.Operators.Momentum
-import PhysLean.QuantumMechanics.OneDimension.Operators.Parity
-import PhysLean.QuantumMechanics.OneDimension.Operators.Position
-import PhysLean.QuantumMechanics.OneDimension.Operators.Unbounded
-import PhysLean.QuantumMechanics.OneDimension.ReflectionlessPotential.Basic
-import PhysLean.QuantumMechanics.PlanckConstant
-import PhysLean.Relativity.Bispinors.Basic
-import PhysLean.Relativity.CliffordAlgebra
-import PhysLean.Relativity.LorentzAlgebra.Basic
-import PhysLean.Relativity.LorentzAlgebra.Basis
-import PhysLean.Relativity.LorentzAlgebra.ExponentialMap
-import PhysLean.Relativity.LorentzGroup.Basic
-import PhysLean.Relativity.LorentzGroup.Boosts.Apply
-import PhysLean.Relativity.LorentzGroup.Boosts.Basic
-import PhysLean.Relativity.LorentzGroup.Boosts.Generalized
-import PhysLean.Relativity.LorentzGroup.Orthochronous.Basic
-import PhysLean.Relativity.LorentzGroup.Proper
-import PhysLean.Relativity.LorentzGroup.Restricted.Basic
-import PhysLean.Relativity.LorentzGroup.Restricted.FromBoostRotation
-import PhysLean.Relativity.LorentzGroup.Rotations
-import PhysLean.Relativity.LorentzGroup.ToVector
-import PhysLean.Relativity.MinkowskiMatrix
-import PhysLean.Relativity.PauliMatrices.AsTensor
-import PhysLean.Relativity.PauliMatrices.Basic
-import PhysLean.Relativity.PauliMatrices.CliffordAlgebra
-import PhysLean.Relativity.PauliMatrices.Relations
-import PhysLean.Relativity.PauliMatrices.SelfAdjoint
-import PhysLean.Relativity.PauliMatrices.ToTensor
-import PhysLean.Relativity.SL2C.Basic
-import PhysLean.Relativity.SL2C.SelfAdjoint
-import PhysLean.Relativity.Special.ProperTime
-import PhysLean.Relativity.Special.TwinParadox.Basic
-import PhysLean.Relativity.SpeedOfLight
-import PhysLean.Relativity.Tensors.Basic
-import PhysLean.Relativity.Tensors.Color.Basic
-import PhysLean.Relativity.Tensors.Color.Discrete
-import PhysLean.Relativity.Tensors.Color.Lift
-import PhysLean.Relativity.Tensors.ComplexTensor.Basic
-import PhysLean.Relativity.Tensors.ComplexTensor.Lemmas
-import PhysLean.Relativity.Tensors.ComplexTensor.Matrix.Pre
-import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Basic
-import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Lemmas
-import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Pre
-import PhysLean.Relativity.Tensors.ComplexTensor.OfRat
-import PhysLean.Relativity.Tensors.ComplexTensor.Units.Basic
-import PhysLean.Relativity.Tensors.ComplexTensor.Units.Pre
-import PhysLean.Relativity.Tensors.ComplexTensor.Units.Symm
-import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic
-import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction
-import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules
-import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Basic
-import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Contraction
-import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Metric
-import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Modules
-import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Two
-import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Unit
-import PhysLean.Relativity.Tensors.Constructors
-import PhysLean.Relativity.Tensors.Contraction.Basic
-import PhysLean.Relativity.Tensors.Contraction.Basis
-import PhysLean.Relativity.Tensors.Contraction.Products
-import PhysLean.Relativity.Tensors.Contraction.Pure
-import PhysLean.Relativity.Tensors.Dual
-import PhysLean.Relativity.Tensors.Elab
-import PhysLean.Relativity.Tensors.Evaluation
-import PhysLean.Relativity.Tensors.MetricTensor
-import PhysLean.Relativity.Tensors.OfInt
-import PhysLean.Relativity.Tensors.Product
-import PhysLean.Relativity.Tensors.RealTensor.Basic
-import PhysLean.Relativity.Tensors.RealTensor.CoVector.Basic
-import PhysLean.Relativity.Tensors.RealTensor.Derivative
-import PhysLean.Relativity.Tensors.RealTensor.Matrix.Pre
-import PhysLean.Relativity.Tensors.RealTensor.Metrics.Basic
-import PhysLean.Relativity.Tensors.RealTensor.Metrics.Pre
-import PhysLean.Relativity.Tensors.RealTensor.ToComplex
-import PhysLean.Relativity.Tensors.RealTensor.Units.Pre
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Basic
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.Basic
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
-import PhysLean.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Basic
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
-import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Modules
-import PhysLean.Relativity.Tensors.RealTensor.Velocity.Basic
-import PhysLean.Relativity.Tensors.TensorSpecies.Basic
-import PhysLean.Relativity.Tensors.Tensorial
-import PhysLean.Relativity.Tensors.UnitTensor
-import PhysLean.SpaceAndTime.Space.Basic
-import PhysLean.SpaceAndTime.Space.ConstantSliceDist
-import PhysLean.SpaceAndTime.Space.CrossProduct
-import PhysLean.SpaceAndTime.Space.Derivatives.Basic
-import PhysLean.SpaceAndTime.Space.Derivatives.Curl
-import PhysLean.SpaceAndTime.Space.Derivatives.Div
-import PhysLean.SpaceAndTime.Space.Derivatives.Grad
-import PhysLean.SpaceAndTime.Space.Derivatives.Laplacian
-import PhysLean.SpaceAndTime.Space.DistConst
-import PhysLean.SpaceAndTime.Space.DistOfFunction
-import PhysLean.SpaceAndTime.Space.Integrals.Basic
-import PhysLean.SpaceAndTime.Space.Integrals.RadialAngularMeasure
-import PhysLean.SpaceAndTime.Space.IsDistBounded
-import PhysLean.SpaceAndTime.Space.LengthUnit
-import PhysLean.SpaceAndTime.Space.Module
-import PhysLean.SpaceAndTime.Space.Norm
-import PhysLean.SpaceAndTime.Space.Slice
-import PhysLean.SpaceAndTime.Space.Translations
-import PhysLean.SpaceAndTime.SpaceTime.Basic
-import PhysLean.SpaceAndTime.SpaceTime.Boosts
-import PhysLean.SpaceAndTime.SpaceTime.Derivatives
-import PhysLean.SpaceAndTime.SpaceTime.LorentzAction
-import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
-import PhysLean.SpaceAndTime.Time.Basic
-import PhysLean.SpaceAndTime.Time.Derivatives
-import PhysLean.SpaceAndTime.Time.TimeMan
-import PhysLean.SpaceAndTime.Time.TimeTransMan
-import PhysLean.SpaceAndTime.Time.TimeUnit
-import PhysLean.SpaceAndTime.TimeAndSpace.Basic
-import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
-import PhysLean.StatisticalMechanics.BoltzmannConstant
-import PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic
-import PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite
-import PhysLean.StatisticalMechanics.CanonicalEnsemble.Lemmas
-import PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState
-import PhysLean.StringTheory.Basic
-import PhysLean.StringTheory.FTheory.SU5.Basic
-import PhysLean.StringTheory.FTheory.SU5.Charges.AnomalyFree
-import PhysLean.StringTheory.FTheory.SU5.Charges.OfRationalSection
-import PhysLean.StringTheory.FTheory.SU5.Charges.Viable
-import PhysLean.StringTheory.FTheory.SU5.Fluxes.Basic
-import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
-import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness
-import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
-import PhysLean.StringTheory.FTheory.SU5.Quanta.Basic
-import PhysLean.StringTheory.FTheory.SU5.Quanta.FiveQuanta
-import PhysLean.StringTheory.FTheory.SU5.Quanta.IsViable
-import PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta
-import PhysLean.Thermodynamics.Basic
-import PhysLean.Thermodynamics.IdealGas.Basic
-import PhysLean.Thermodynamics.Temperature.Basic
-import PhysLean.Thermodynamics.Temperature.TemperatureUnits
-import PhysLean.Units.Basic
-import PhysLean.Units.Dimension
-import PhysLean.Units.Examples
-import PhysLean.Units.FDeriv
-import PhysLean.Units.Integral
-import PhysLean.Units.UnitDependent
-import PhysLean.Units.WithDim.Area
-import PhysLean.Units.WithDim.Basic
-import PhysLean.Units.WithDim.Energy
-import PhysLean.Units.WithDim.Mass
-import PhysLean.Units.WithDim.Momentum
-import PhysLean.Units.WithDim.Pressure
-import PhysLean.Units.WithDim.Speed
-import PhysLean.Units.WithDim.Velocity
+module
+
+public import PhysLean.ClassicalMechanics.Basic
+public import PhysLean.ClassicalMechanics.DampedHarmonicOscillator.Basic
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.Solution
+public import PhysLean.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence
+public import PhysLean.ClassicalMechanics.Mass.MassUnit
+public import PhysLean.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
+public import PhysLean.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
+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.Vibrations.LinearTriatomic
+public import PhysLean.ClassicalMechanics.WaveEquation.Basic
+public import PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
+public import PhysLean.CondensedMatter.Basic
+public import PhysLean.CondensedMatter.TightBindingChain.Basic
+public import PhysLean.Cosmology.Basic
+public import PhysLean.Cosmology.FLRW.Basic
+public import PhysLean.Electromagnetism.Basic
+public import PhysLean.Electromagnetism.Charge.ChargeUnit
+public import PhysLean.Electromagnetism.Current.CircularCoil
+public import PhysLean.Electromagnetism.Current.InfiniteWire
+public import PhysLean.Electromagnetism.Dynamics.Basic
+public import PhysLean.Electromagnetism.Dynamics.CurrentDensity
+public import PhysLean.Electromagnetism.Dynamics.Hamiltonian
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
+public import PhysLean.Electromagnetism.Dynamics.KineticTerm
+public import PhysLean.Electromagnetism.Dynamics.Lagrangian
+public import PhysLean.Electromagnetism.Kinematics.Boosts
+public import PhysLean.Electromagnetism.Kinematics.EMPotential
+public import PhysLean.Electromagnetism.Kinematics.ElectricField
+public import PhysLean.Electromagnetism.Kinematics.FieldStrength
+public import PhysLean.Electromagnetism.Kinematics.MagneticField
+public import PhysLean.Electromagnetism.Kinematics.ScalarPotential
+public import PhysLean.Electromagnetism.Kinematics.VectorPotential
+public import PhysLean.Electromagnetism.PointParticle.OneDimension
+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.Mathematics.Calculus.AdjFDeriv
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.Mathematics.DataStructures.FourTree.Basic
+public import PhysLean.Mathematics.DataStructures.FourTree.UniqueMap
+public import PhysLean.Mathematics.DataStructures.Matrix.LieTrace
+public import PhysLean.Mathematics.Distribution.Basic
+public import PhysLean.Mathematics.Distribution.PowMul
+public import PhysLean.Mathematics.FDerivCurry
+public import PhysLean.Mathematics.Fin
+public import PhysLean.Mathematics.Fin.Involutions
+public import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
+public import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
+public import PhysLean.Mathematics.InnerProductSpace.Adjoint
+public import PhysLean.Mathematics.InnerProductSpace.Basic
+public import PhysLean.Mathematics.InnerProductSpace.Calculus
+public import PhysLean.Mathematics.InnerProductSpace.Submodule
+public import PhysLean.Mathematics.KroneckerDelta
+public import PhysLean.Mathematics.LinearMaps
+public import PhysLean.Mathematics.List
+public import PhysLean.Mathematics.List.InsertIdx
+public import PhysLean.Mathematics.List.InsertionSort
+public import PhysLean.Mathematics.PiTensorProduct
+public import PhysLean.Mathematics.RatComplexNum
+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
+public import PhysLean.Meta.Informal.Post
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.Meta.Linters.Sorry
+public import PhysLean.Meta.Notes.Basic
+public import PhysLean.Meta.Notes.HTMLNote
+public import PhysLean.Meta.Notes.NoteFile
+public import PhysLean.Meta.Notes.ToHTML
+public import PhysLean.Meta.Remark.Basic
+public import PhysLean.Meta.Remark.Properties
+public import PhysLean.Meta.Sorry
+public import PhysLean.Meta.TODO.Basic
+public import PhysLean.Meta.TransverseTactics
+public import PhysLean.Optics.Basic
+public import PhysLean.Optics.Polarization.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.PatiSalam.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.FamilyMaps
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BoundPlaneDim
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol
+public import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
+public import PhysLean.Particles.BeyondTheStandardModel.Spin10.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
+public import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GramMatrix
+public import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Potential
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.Basic
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.Relations
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.Rows
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
+public import PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
+public import PhysLean.Particles.NeutrinoPhysics.Basic
+public import PhysLean.Particles.StandardModel.AnomalyCancellation.Basic
+public import PhysLean.Particles.StandardModel.AnomalyCancellation.FamilyMaps
+public import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
+public import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas
+public import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization
+public import PhysLean.Particles.StandardModel.AnomalyCancellation.Permutations
+public import PhysLean.Particles.StandardModel.Basic
+public import PhysLean.Particles.StandardModel.HiggsBoson.Basic
+public import PhysLean.Particles.StandardModel.HiggsBoson.Potential
+public import PhysLean.Particles.StandardModel.Representations
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.HyperCharge
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations
+public import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Map
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimalSuperSet
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.FinsetTerms
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfFieldLabel
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfPotentialTerm
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoClosed
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrained
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa
+public import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.ZMod
+public import PhysLean.Particles.SuperSymmetry.SU5.FieldLabels
+public import PhysLean.Particles.SuperSymmetry.SU5.Potential
+public import PhysLean.QFT.AnomalyCancellation.Basic
+public import PhysLean.QFT.AnomalyCancellation.GroupActions
+public import PhysLean.QFT.PerturbationTheory.CreateAnnihilate
+public import PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Basic
+public import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic
+public import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading
+public import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
+public import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
+public import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
+public import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
+public import PhysLean.QFT.PerturbationTheory.FieldSpecification.Basic
+public import PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp
+public import PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnSection
+public import PhysLean.QFT.PerturbationTheory.FieldSpecification.Filters
+public import PhysLean.QFT.PerturbationTheory.FieldSpecification.NormalOrder
+public import PhysLean.QFT.PerturbationTheory.FieldSpecification.TimeOrder
+public import PhysLean.QFT.PerturbationTheory.FieldStatistics.Basic
+public import PhysLean.QFT.PerturbationTheory.FieldStatistics.ExchangeSign
+public import PhysLean.QFT.PerturbationTheory.FieldStatistics.OfFinset
+public import PhysLean.QFT.PerturbationTheory.Koszul.KoszulSign
+public import PhysLean.QFT.PerturbationTheory.Koszul.KoszulSignInsert
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.Grading
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTerm
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTheorem
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.SuperCommute
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeContraction
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeOrder
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.Universality
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.WickTerm
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
+public import PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheoremNormal
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Basic
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Card
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Erase
+public import PhysLean.QFT.PerturbationTheory.WickContraction.ExtractEquiv
+public import PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContract
+public import PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Involutions
+public import PhysLean.QFT.PerturbationTheory.WickContraction.IsFull
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Join
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Perm
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Basic
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Join
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Singleton
+public import PhysLean.QFT.PerturbationTheory.WickContraction.StaticContract
+public import PhysLean.QFT.PerturbationTheory.WickContraction.SubContraction
+public import PhysLean.QFT.PerturbationTheory.WickContraction.TimeCond
+public import PhysLean.QFT.PerturbationTheory.WickContraction.TimeContract
+public import PhysLean.QFT.PerturbationTheory.WickContraction.Uncontracted
+public import PhysLean.QFT.PerturbationTheory.WickContraction.UncontractedList
+public import PhysLean.QFT.QED.AnomalyCancellation.Basic
+public import PhysLean.QFT.QED.AnomalyCancellation.BasisLinear
+public import PhysLean.QFT.QED.AnomalyCancellation.ConstAbs
+public import PhysLean.QFT.QED.AnomalyCancellation.Even.BasisLinear
+public import PhysLean.QFT.QED.AnomalyCancellation.Even.LineInCubic
+public import PhysLean.QFT.QED.AnomalyCancellation.Even.Parameterization
+public import PhysLean.QFT.QED.AnomalyCancellation.LineInPlaneCond
+public import PhysLean.QFT.QED.AnomalyCancellation.LowDim.One
+public import PhysLean.QFT.QED.AnomalyCancellation.LowDim.Three
+public import PhysLean.QFT.QED.AnomalyCancellation.LowDim.Two
+public import PhysLean.QFT.QED.AnomalyCancellation.Odd.BasisLinear
+public import PhysLean.QFT.QED.AnomalyCancellation.Odd.LineInCubic
+public import PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
+public import PhysLean.QFT.QED.AnomalyCancellation.Permutations
+public import PhysLean.QFT.QED.AnomalyCancellation.Sorts
+public import PhysLean.QFT.QED.AnomalyCancellation.VectorLike
+public import PhysLean.QuantumMechanics.DDimensions.Hydrogen.Basic
+public import PhysLean.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVector
+public import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
+public import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation
+public import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+public import PhysLean.QuantumMechanics.DDimensions.Operators.Position
+public import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
+public import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
+public import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
+public import PhysLean.QuantumMechanics.FiniteTarget.Basic
+public import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
+public import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
+public import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
+public import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
+public import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+public import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Examples
+public import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
+public import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+public import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
+public import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PlaneWaves
+public import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PositionStates
+public import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
+public import PhysLean.QuantumMechanics.OneDimension.Operators.Commutation
+public import PhysLean.QuantumMechanics.OneDimension.Operators.Momentum
+public import PhysLean.QuantumMechanics.OneDimension.Operators.Parity
+public import PhysLean.QuantumMechanics.OneDimension.Operators.Position
+public import PhysLean.QuantumMechanics.OneDimension.Operators.Unbounded
+public import PhysLean.QuantumMechanics.OneDimension.ReflectionlessPotential.Basic
+public import PhysLean.QuantumMechanics.PlanckConstant
+public import PhysLean.Relativity.Bispinors.Basic
+public import PhysLean.Relativity.CliffordAlgebra
+public import PhysLean.Relativity.LorentzAlgebra.Basic
+public import PhysLean.Relativity.LorentzAlgebra.Basis
+public import PhysLean.Relativity.LorentzAlgebra.ExponentialMap
+public import PhysLean.Relativity.LorentzGroup.Basic
+public import PhysLean.Relativity.LorentzGroup.Boosts.Apply
+public import PhysLean.Relativity.LorentzGroup.Boosts.Basic
+public import PhysLean.Relativity.LorentzGroup.Boosts.Generalized
+public import PhysLean.Relativity.LorentzGroup.Orthochronous.Basic
+public import PhysLean.Relativity.LorentzGroup.Proper
+public import PhysLean.Relativity.LorentzGroup.Restricted.Basic
+public import PhysLean.Relativity.LorentzGroup.Restricted.FromBoostRotation
+public import PhysLean.Relativity.LorentzGroup.Rotations
+public import PhysLean.Relativity.LorentzGroup.ToVector
+public import PhysLean.Relativity.MinkowskiMatrix
+public import PhysLean.Relativity.PauliMatrices.AsTensor
+public import PhysLean.Relativity.PauliMatrices.Basic
+public import PhysLean.Relativity.PauliMatrices.CliffordAlgebra
+public import PhysLean.Relativity.PauliMatrices.Relations
+public import PhysLean.Relativity.PauliMatrices.SelfAdjoint
+public import PhysLean.Relativity.PauliMatrices.ToTensor
+public import PhysLean.Relativity.SL2C.Basic
+public import PhysLean.Relativity.SL2C.SelfAdjoint
+public import PhysLean.Relativity.Special.ProperTime
+public import PhysLean.Relativity.Special.TwinParadox.Basic
+public import PhysLean.Relativity.SpeedOfLight
+public import PhysLean.Relativity.Tensors.Basic
+public import PhysLean.Relativity.Tensors.Color.Basic
+public import PhysLean.Relativity.Tensors.Color.Discrete
+public import PhysLean.Relativity.Tensors.Color.Lift
+public import PhysLean.Relativity.Tensors.ComplexTensor.Basic
+public import PhysLean.Relativity.Tensors.ComplexTensor.Lemmas
+public import PhysLean.Relativity.Tensors.ComplexTensor.Matrix.Pre
+public import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Basic
+public import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Lemmas
+public import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Pre
+public import PhysLean.Relativity.Tensors.ComplexTensor.OfRat
+public import PhysLean.Relativity.Tensors.ComplexTensor.Units.Basic
+public import PhysLean.Relativity.Tensors.ComplexTensor.Units.Pre
+public import PhysLean.Relativity.Tensors.ComplexTensor.Units.Symm
+public import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic
+public import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction
+public import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules
+public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Basic
+public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Contraction
+public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Metric
+public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Modules
+public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Two
+public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Unit
+public import PhysLean.Relativity.Tensors.Constructors
+public import PhysLean.Relativity.Tensors.Contraction.Basic
+public import PhysLean.Relativity.Tensors.Contraction.Basis
+public import PhysLean.Relativity.Tensors.Contraction.Products
+public import PhysLean.Relativity.Tensors.Contraction.Pure
+public import PhysLean.Relativity.Tensors.Dual
+public import PhysLean.Relativity.Tensors.Elab
+public import PhysLean.Relativity.Tensors.Evaluation
+public import PhysLean.Relativity.Tensors.MetricTensor
+public import PhysLean.Relativity.Tensors.OfInt
+public import PhysLean.Relativity.Tensors.Product
+public import PhysLean.Relativity.Tensors.RealTensor.Basic
+public import PhysLean.Relativity.Tensors.RealTensor.CoVector.Basic
+public import PhysLean.Relativity.Tensors.RealTensor.Derivative
+public import PhysLean.Relativity.Tensors.RealTensor.Matrix.Pre
+public import PhysLean.Relativity.Tensors.RealTensor.Metrics.Basic
+public import PhysLean.Relativity.Tensors.RealTensor.Metrics.Pre
+public import PhysLean.Relativity.Tensors.RealTensor.ToComplex
+public import PhysLean.Relativity.Tensors.RealTensor.Units.Pre
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Basic
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.Basic
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Basic
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
+public import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Modules
+public import PhysLean.Relativity.Tensors.RealTensor.Velocity.Basic
+public import PhysLean.Relativity.Tensors.TensorSpecies.Basic
+public import PhysLean.Relativity.Tensors.Tensorial
+public import PhysLean.Relativity.Tensors.UnitTensor
+public import PhysLean.SpaceAndTime.Space.Basic
+public import PhysLean.SpaceAndTime.Space.ConstantSliceDist
+public import PhysLean.SpaceAndTime.Space.CrossProduct
+public import PhysLean.SpaceAndTime.Space.Derivatives.Basic
+public import PhysLean.SpaceAndTime.Space.Derivatives.Curl
+public import PhysLean.SpaceAndTime.Space.Derivatives.Div
+public import PhysLean.SpaceAndTime.Space.Derivatives.Grad
+public import PhysLean.SpaceAndTime.Space.Derivatives.Laplacian
+public import PhysLean.SpaceAndTime.Space.DistConst
+public import PhysLean.SpaceAndTime.Space.DistOfFunction
+public import PhysLean.SpaceAndTime.Space.Integrals.Basic
+public import PhysLean.SpaceAndTime.Space.Integrals.RadialAngularMeasure
+public import PhysLean.SpaceAndTime.Space.IsDistBounded
+public import PhysLean.SpaceAndTime.Space.LengthUnit
+public import PhysLean.SpaceAndTime.Space.Module
+public import PhysLean.SpaceAndTime.Space.Norm
+public import PhysLean.SpaceAndTime.Space.Slice
+public import PhysLean.SpaceAndTime.Space.Translations
+public import PhysLean.SpaceAndTime.SpaceTime.Basic
+public import PhysLean.SpaceAndTime.SpaceTime.Boosts
+public import PhysLean.SpaceAndTime.SpaceTime.Derivatives
+public import PhysLean.SpaceAndTime.SpaceTime.LorentzAction
+public import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
+public import PhysLean.SpaceAndTime.Time.Basic
+public import PhysLean.SpaceAndTime.Time.Derivatives
+public import PhysLean.SpaceAndTime.Time.TimeMan
+public import PhysLean.SpaceAndTime.Time.TimeTransMan
+public import PhysLean.SpaceAndTime.Time.TimeUnit
+public import PhysLean.SpaceAndTime.TimeAndSpace.Basic
+public import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
+public import PhysLean.StatisticalMechanics.BoltzmannConstant
+public import PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic
+public import PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite
+public import PhysLean.StatisticalMechanics.CanonicalEnsemble.Lemmas
+public import PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState
+public import PhysLean.StringTheory.Basic
+public import PhysLean.StringTheory.FTheory.SU5.Basic
+public import PhysLean.StringTheory.FTheory.SU5.Charges.AnomalyFree
+public import PhysLean.StringTheory.FTheory.SU5.Charges.OfRationalSection
+public import PhysLean.StringTheory.FTheory.SU5.Charges.Viable
+public import PhysLean.StringTheory.FTheory.SU5.Fluxes.Basic
+public import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
+public import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness
+public import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
+public import PhysLean.StringTheory.FTheory.SU5.Quanta.Basic
+public import PhysLean.StringTheory.FTheory.SU5.Quanta.FiveQuanta
+public import PhysLean.StringTheory.FTheory.SU5.Quanta.IsViable
+public import PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta
+public import PhysLean.Thermodynamics.Basic
+public import PhysLean.Thermodynamics.IdealGas.Basic
+public import PhysLean.Thermodynamics.Temperature.Basic
+public import PhysLean.Thermodynamics.Temperature.TemperatureUnits
+public import PhysLean.Units.Basic
+public import PhysLean.Units.Dimension
+public import PhysLean.Units.Examples
+public import PhysLean.Units.FDeriv
+public import PhysLean.Units.Integral
+public import PhysLean.Units.UnitDependent
+public import PhysLean.Units.WithDim.Area
+public import PhysLean.Units.WithDim.Basic
+public import PhysLean.Units.WithDim.Energy
+public import PhysLean.Units.WithDim.Mass
+public import PhysLean.Units.WithDim.Momentum
+public import PhysLean.Units.WithDim.Pressure
+public import PhysLean.Units.WithDim.Speed
+public import PhysLean.Units.WithDim.Velocity
diff --git a/PhysLean/ClassicalMechanics/Basic.lean b/PhysLean/ClassicalMechanics/Basic.lean
index 6159772f2..a731dfe92 100644
--- a/PhysLean/ClassicalMechanics/Basic.lean
+++ b/PhysLean/ClassicalMechanics/Basic.lean
@@ -3,6 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
+module
+
/-!
# Classical mechanics
@@ -10,4 +12,4 @@ Authors: Joseph Tooby-Smith
This file is currently a stub.
Please feel free to contribute!
--/
+-/@[expose] public section
diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
index 728e3d42e..e0c07586b 100644
--- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
+++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Nicola Bernini. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nicola Bernini
-/
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
+module
+
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
/-!
# The Damped Harmonic Oscillator
@@ -59,6 +61,8 @@ References for the damped harmonic oscillator include:
-/
+@[expose] public section
+
namespace ClassicalMechanics
open Real
open ContDiff
diff --git a/PhysLean/ClassicalMechanics/EulerLagrange.lean b/PhysLean/ClassicalMechanics/EulerLagrange.lean
index d1c75fdbe..c81837a69 100644
--- a/PhysLean/ClassicalMechanics/EulerLagrange.lean
+++ b/PhysLean/ClassicalMechanics/EulerLagrange.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
/-!
# Euler-Lagrange equations
@@ -14,6 +16,8 @@ and prove the that the variational derivative of the action functional
-/
+@[expose] public section
+
open MeasureTheory ContDiff InnerProductSpace Time
variable {X} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]
diff --git a/PhysLean/ClassicalMechanics/HamiltonsEquations.lean b/PhysLean/ClassicalMechanics/HamiltonsEquations.lean
index 0c5edb7d0..e43db2339 100644
--- a/PhysLean/ClassicalMechanics/HamiltonsEquations.lean
+++ b/PhysLean/ClassicalMechanics/HamiltonsEquations.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
/-!
# Hamilton's equations
@@ -23,6 +25,8 @@ applied to `(p, q)`.
-/
+@[expose] public section
+
open MeasureTheory ContDiff InnerProductSpace Time
namespace ClassicalMechanics
diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
index 5d7b4a39e..8c1a20f2e 100644
--- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
+++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith, Lode Vermeulen
-/
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
-import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
+module
+
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
/-!
# The Classical Harmonic Oscillator
@@ -81,6 +83,8 @@ References for the classical harmonic oscillator include:
-/
+@[expose] public section
+
namespace ClassicalMechanics
open Real
open Space
diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
index 4ae1e08d3..bf6394ac8 100644
--- a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
+++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
@@ -3,8 +3,10 @@ Copyright (c) 2026 Nicola Bernini. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nicola Bernini
-/
-import Mathlib.Geometry.Manifold.Diffeomorph
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import PhysLean.SpaceAndTime.Time.Basic
/-!
# Configuration space of the harmonic oscillator
@@ -12,6 +14,8 @@ The configuration space is defined as a one-dimensional smooth manifold,
modeled on `ℝ`, with a chosen coordinate.
-/
+@[expose] public section
+
namespace ClassicalMechanics
namespace HarmonicOscillator
diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean
index 276fab0d9..50ce13332 100644
--- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean
+++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith, Lode Vermeulen
-/
-import Mathlib.Analysis.CStarAlgebra.Classes
-import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
-import PhysLean.Units.Basic
+module
+
+public import Mathlib.Analysis.CStarAlgebra.Classes
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
+public import PhysLean.Units.Basic
/-!
# Solutions to the classical harmonic oscillator
@@ -53,6 +55,8 @@ References for the classical harmonic oscillator include:
-/
+@[expose] public section
+
namespace ClassicalMechanics
open Real Time ContDiff
diff --git a/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean b/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
index a3f2679bc..9d60d665c 100644
--- a/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
+++ b/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Rein Zustand. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rein Zustand
-/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
/-!
# Equivalent Lagrangians under Total Derivatives
@@ -51,6 +53,8 @@ This is because:
-/
+@[expose] public section
+
namespace ClassicalMechanics
open InnerProductSpace
diff --git a/PhysLean/ClassicalMechanics/Mass/MassUnit.lean b/PhysLean/ClassicalMechanics/Mass/MassUnit.lean
index 4eee024bd..8a4a96a33 100644
--- a/PhysLean/ClassicalMechanics/Mass/MassUnit.lean
+++ b/PhysLean/ClassicalMechanics/Mass/MassUnit.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Geometry.Manifold.Diffeomorph
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import PhysLean.SpaceAndTime.Time.Basic
/-!
# Units on Mass
@@ -24,6 +26,8 @@ existence of the mass unit of kilograms, and construct all other mass units from
-/
+@[expose] public section
+
open NNReal
/-- The choices of translationally-invariant metrics on the mass-manifold.
diff --git a/PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean b/PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean
index 4fe0da0c7..063e67a7b 100644
--- a/PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean
+++ b/PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shlok Vaibhav Singh
-/
-import PhysLean.Meta.Informal.Basic
-import PhysLean.Meta.Sorry
+module
+
+public import PhysLean.Meta.Informal.Basic
+public import PhysLean.Meta.Sorry
/-!
# Coplanar Double Pendulum
### Tag: LnL_1.5.1
@@ -62,6 +64,8 @@ so that the Lagrangian becomes:
$$
-/
+@[expose] public section
+
namespace ClassicalMechanics
namespace CoplanarDoublePendulum
diff --git a/PhysLean/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean b/PhysLean/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean
index 02962f19a..ad8facf17 100644
--- a/PhysLean/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean
+++ b/PhysLean/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean
@@ -3,6 +3,8 @@ Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shlok Vaibhav Singh
-/
+module
+
/-!
# Miscellaneous Pendulum Pivot Motions
### Tag: LnL_1.5.3
@@ -139,7 +141,7 @@ Ignoring the total time derivate term, the final lagrangian becomes:
$$
L = \tfrac{1}{2} m l^2\dot{\phi}^2 + m g l \cos\phi - m a l \gamma^2 \cos\phi\cos(\gamma t)
$$
--/
+-/@[expose] public section
namespace ClassicalMechanics
diff --git a/PhysLean/ClassicalMechanics/Pendulum/SlidingPendulum.lean b/PhysLean/ClassicalMechanics/Pendulum/SlidingPendulum.lean
index 062fa321d..69a447774 100644
--- a/PhysLean/ClassicalMechanics/Pendulum/SlidingPendulum.lean
+++ b/PhysLean/ClassicalMechanics/Pendulum/SlidingPendulum.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shlok Vaibhav Singh
-/
-import PhysLean.Meta.Sorry
+module
+
+public import PhysLean.Meta.Sorry
/-!
# Sliding Pendulum
### Tag: LnL_1.5.2
@@ -55,6 +57,8 @@ $$
-/
+@[expose] public section
+
namespace ClassicalMechanics
namespace SlidingPendulum
diff --git a/PhysLean/ClassicalMechanics/RigidBody/Basic.lean b/PhysLean/ClassicalMechanics/RigidBody/Basic.lean
index dd3ddc073..e59b1e516 100644
--- a/PhysLean/ClassicalMechanics/RigidBody/Basic.lean
+++ b/PhysLean/ClassicalMechanics/RigidBody/Basic.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.SpaceAndTime.Space.Derivatives.Curl
-import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
+module
+
+public import PhysLean.SpaceAndTime.Space.Derivatives.Curl
+public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-!
# Rigid bodies
@@ -21,6 +23,8 @@ In this module we will define the basic properties of a rigid body, including
- Landau and Lifshitz, Mechanics, page 100, Section 32
-/
+@[expose] public section
+
open Manifold
TODO "MEX5S" "The definition of a rigid body is currently defined via linear maps
diff --git a/PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean b/PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean
index 970d8e410..a46cea817 100644
--- a/PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean
+++ b/PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.ClassicalMechanics.RigidBody.Basic
+module
+
+public import PhysLean.ClassicalMechanics.RigidBody.Basic
/-!
# The solid sphere as a rigid body
@@ -13,6 +15,8 @@ center of mass and inertia tensor.
-/
+@[expose] public section
+
open Manifold
open MeasureTheory
namespace RigidBody
diff --git a/PhysLean/ClassicalMechanics/Scattering/RigidSphere.lean b/PhysLean/ClassicalMechanics/Scattering/RigidSphere.lean
index 16e566849..b79e973fc 100644
--- a/PhysLean/ClassicalMechanics/Scattering/RigidSphere.lean
+++ b/PhysLean/ClassicalMechanics/Scattering/RigidSphere.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.TODO.Basic
+module
+
+public import PhysLean.Meta.TODO.Basic
/-!
# Scattering off a perfectly rigid sphere
@@ -13,4 +15,6 @@ import PhysLean.Meta.TODO.Basic
- Landau and Lifshitz, Mechanics, page 50, Section 18, Problem 1
-/
+@[expose] public section
+
TODO "L7OTP" "Derive the scattering cross section of a perfectly rigid sphere."
diff --git a/PhysLean/ClassicalMechanics/Vibrations/LinearTriatomic.lean b/PhysLean/ClassicalMechanics/Vibrations/LinearTriatomic.lean
index af88fbcd9..5a234986c 100644
--- a/PhysLean/ClassicalMechanics/Vibrations/LinearTriatomic.lean
+++ b/PhysLean/ClassicalMechanics/Vibrations/LinearTriatomic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.TODO.Basic
+module
+
+public import PhysLean.Meta.TODO.Basic
/-!
# Vibrations of a symmetric linear triatomic molecule
@@ -13,4 +15,6 @@ import PhysLean.Meta.TODO.Basic
- Landau and Lifshitz, Mechanics, page 72, Section 24, Problem 1
-/
+@[expose] public section
+
TODO "L7O4I" "Derive the frequencies of vibaration of a symmetric linear triatomic molecule."
diff --git a/PhysLean/ClassicalMechanics/WaveEquation/Basic.lean b/PhysLean/ClassicalMechanics/WaveEquation/Basic.lean
index a3687d8ba..d2b98925e 100644
--- a/PhysLean/ClassicalMechanics/WaveEquation/Basic.lean
+++ b/PhysLean/ClassicalMechanics/WaveEquation/Basic.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong
-/
-import PhysLean.SpaceAndTime.Space.CrossProduct
-import PhysLean.SpaceAndTime.TimeAndSpace.Basic
+module
+
+public import PhysLean.SpaceAndTime.Space.CrossProduct
+public import PhysLean.SpaceAndTime.TimeAndSpace.Basic
/-!
# Wave equation
@@ -39,6 +41,8 @@ By a plne wave we mean a function of the form `f(t, x) = f₀(⟪x, s⟫_ℝ - c
-/
+@[expose] public section
+
namespace ClassicalMechanics
open Space
diff --git a/PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean b/PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean
index e97044ead..9e25a2b3a 100644
--- a/PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean
+++ b/PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong
-/
-import PhysLean.ClassicalMechanics.WaveEquation.Basic
+module
+
+public import PhysLean.ClassicalMechanics.WaveEquation.Basic
/-!
# Harmonic Wave
@@ -15,6 +17,8 @@ the status of Fourier theory in Mathlib.
-/
+@[expose] public section
+
namespace ClassicalMechanics
open Space
diff --git a/PhysLean/CondensedMatter/Basic.lean b/PhysLean/CondensedMatter/Basic.lean
index 03b8b831b..837df4a87 100644
--- a/PhysLean/CondensedMatter/Basic.lean
+++ b/PhysLean/CondensedMatter/Basic.lean
@@ -3,6 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
+module
+
/-!
# Condensed Matter
@@ -18,4 +20,4 @@ Some directories which are NOT currently place holders are:
- Quantum Mechanics
- Relativity
--/
+-/@[expose] public section
diff --git a/PhysLean/CondensedMatter/TightBindingChain/Basic.lean b/PhysLean/CondensedMatter/TightBindingChain/Basic.lean
index 9efa879a9..8c016bb98 100644
--- a/PhysLean/CondensedMatter/TightBindingChain/Basic.lean
+++ b/PhysLean/CondensedMatter/TightBindingChain/Basic.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.Informal.Basic
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.Meta.Linters.Sorry
-import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
+module
+
+public import PhysLean.Meta.Informal.Basic
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.Meta.Linters.Sorry
+public import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
/-!
# The tight binding chain
@@ -68,6 +70,8 @@ with periodic boundary conditions.
-/
+@[expose] public section
+
namespace CondensedMatter
/-!
diff --git a/PhysLean/Cosmology/Basic.lean b/PhysLean/Cosmology/Basic.lean
index 27649e676..2042ae74f 100644
--- a/PhysLean/Cosmology/Basic.lean
+++ b/PhysLean/Cosmology/Basic.lean
@@ -3,6 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
+module
+
/-!
# Cosmology
@@ -18,4 +20,4 @@ Some directories which are NOT currently place holders are:
- Quantum Mechanics
- Relativity
--/
+-/@[expose] public section
diff --git a/PhysLean/Cosmology/FLRW/Basic.lean b/PhysLean/Cosmology/FLRW/Basic.lean
index 5bef35ced..d65da391f 100644
--- a/PhysLean/Cosmology/FLRW/Basic.lean
+++ b/PhysLean/Cosmology/FLRW/Basic.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luis Gabriel C. Bariuan, Joseph Tooby-Smith
-/
-import PhysLean.SpaceAndTime.Space.Basic
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
+module
+
+public import PhysLean.SpaceAndTime.Space.Basic
+public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-!
# The Friedmann-Lemaître-Robertson-Walker metric
@@ -13,6 +15,8 @@ Parts of this file is currently informal or semiformal.
-/
+@[expose] public section
+
open Filter
open scoped Topology
diff --git a/PhysLean/Electromagnetism/Basic.lean b/PhysLean/Electromagnetism/Basic.lean
index 7ef982c70..74ba09220 100644
--- a/PhysLean/Electromagnetism/Basic.lean
+++ b/PhysLean/Electromagnetism/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.SpaceAndTime.SpaceTime.Basic
+module
+
+public import PhysLean.SpaceAndTime.SpaceTime.Basic
/-!
# Electromagnetism
@@ -14,6 +16,8 @@ This module is old and parts of it will soon be replaced.
-/
+@[expose] public section
+
namespace Electromagnetism
/-- The electric field is a map from `d`+1 dimensional spacetime to the vector space
diff --git a/PhysLean/Electromagnetism/Charge/ChargeUnit.lean b/PhysLean/Electromagnetism/Charge/ChargeUnit.lean
index 89ab1848f..5ab755452 100644
--- a/PhysLean/Electromagnetism/Charge/ChargeUnit.lean
+++ b/PhysLean/Electromagnetism/Charge/ChargeUnit.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Algebra.EuclideanDomain.Basic
-import Mathlib.Algebra.EuclideanDomain.Field
-import Mathlib.Analysis.RCLike.Basic
-import PhysLean.Meta.TODO.Basic
+module
+
+public import Mathlib.Algebra.EuclideanDomain.Basic
+public import Mathlib.Algebra.EuclideanDomain.Field
+public import Mathlib.Analysis.RCLike.Basic
+public import PhysLean.Meta.TODO.Basic
/-!
# The units of charge
@@ -30,6 +32,8 @@ existence of the charge unit of the coulomb, and construct all other charge unit
-/
+@[expose] public section
+
open NNReal
/-- The choices of translationally-invariant metrics on the charge-manifold.
diff --git a/PhysLean/Electromagnetism/Current/CircularCoil.lean b/PhysLean/Electromagnetism/Current/CircularCoil.lean
index 99503e2f1..213908793 100644
--- a/PhysLean/Electromagnetism/Current/CircularCoil.lean
+++ b/PhysLean/Electromagnetism/Current/CircularCoil.lean
@@ -3,11 +3,13 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
-import PhysLean.SpaceAndTime.Space.Norm
-import PhysLean.SpaceAndTime.Space.Translations
-import PhysLean.SpaceAndTime.Space.ConstantSliceDist
-import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
+module
+
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
+public import PhysLean.SpaceAndTime.Space.Norm
+public import PhysLean.SpaceAndTime.Space.Translations
+public import PhysLean.SpaceAndTime.Space.ConstantSliceDist
+public import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
/-!
# The electrostatics of a circular coil
@@ -29,6 +31,8 @@ electromagnetic potentials and fields around a circular coil.
-/
+@[expose] public section
+
TODO "TCGIW" "Copying the structure of the electrostatics of an infinite wire,
complete the definitions and proofs for a circular coil carrying a steady current."
diff --git a/PhysLean/Electromagnetism/Current/InfiniteWire.lean b/PhysLean/Electromagnetism/Current/InfiniteWire.lean
index 3f0ee1330..0625682bb 100644
--- a/PhysLean/Electromagnetism/Current/InfiniteWire.lean
+++ b/PhysLean/Electromagnetism/Current/InfiniteWire.lean
@@ -3,11 +3,13 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
-import PhysLean.SpaceAndTime.Space.Norm
-import PhysLean.SpaceAndTime.Space.Translations
-import PhysLean.SpaceAndTime.Space.ConstantSliceDist
-import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
+module
+
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
+public import PhysLean.SpaceAndTime.Space.Norm
+public import PhysLean.SpaceAndTime.Space.Translations
+public import PhysLean.SpaceAndTime.Space.ConstantSliceDist
+public import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
/-!
# The magnetic field around a infinite wire
@@ -39,6 +41,8 @@ carrying a steady current along the x-axis.
-/
+@[expose] public section
+
namespace Electromagnetism
open Distribution SchwartzMap
open Space MeasureTheory
diff --git a/PhysLean/Electromagnetism/Dynamics/Basic.lean b/PhysLean/Electromagnetism/Dynamics/Basic.lean
index 18b673a5f..58e3a1e91 100644
--- a/PhysLean/Electromagnetism/Dynamics/Basic.lean
+++ b/PhysLean/Electromagnetism/Dynamics/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Basic
+module
+
+public import PhysLean.Electromagnetism.Basic
/-!
# Free space
@@ -33,6 +35,8 @@ in free space in terms of these constants.
-/
+@[expose] public section
+
namespace Electromagnetism
/-!
diff --git a/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean b/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean
index c62fa4843..efebb7a5c 100644
--- a/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean
+++ b/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
+module
+
+public import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
/-!
# The Lorentz Current Density
@@ -46,6 +48,8 @@ The current density is given in terms of the charge density `ρ` and the current
-/
+@[expose] public section
+
namespace Electromagnetism
open TensorSpecies
open SpaceTime
diff --git a/PhysLean/Electromagnetism/Dynamics/Hamiltonian.lean b/PhysLean/Electromagnetism/Dynamics/Hamiltonian.lean
index 17a38b4f7..9d43f502b 100644
--- a/PhysLean/Electromagnetism/Dynamics/Hamiltonian.lean
+++ b/PhysLean/Electromagnetism/Dynamics/Hamiltonian.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.Lagrangian
+module
+
+public import PhysLean.Electromagnetism.Dynamics.Lagrangian
/-!
# The Hamiltonian in electromagnetism
@@ -40,6 +42,8 @@ in the case of three spatial dimensions.
- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Dynamics/IsExtrema.lean b/PhysLean/Electromagnetism/Dynamics/IsExtrema.lean
index 799780212..e58a7f5b1 100644
--- a/PhysLean/Electromagnetism/Dynamics/IsExtrema.lean
+++ b/PhysLean/Electromagnetism/Dynamics/IsExtrema.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.Lagrangian
+module
+
+public import PhysLean.Electromagnetism.Dynamics.Lagrangian
/-!
# Extrema of the Lagrangian density
@@ -47,6 +49,8 @@ Maxwell's equations with sources, i.e. Gauss's law and Ampère's law.
## iv. References
-/
+
+@[expose] public section
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Dynamics/KineticTerm.lean b/PhysLean/Electromagnetism/Dynamics/KineticTerm.lean
index aed2091a9..3928e83ec 100644
--- a/PhysLean/Electromagnetism/Dynamics/KineticTerm.lean
+++ b/PhysLean/Electromagnetism/Dynamics/KineticTerm.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.MagneticField
-import PhysLean.Electromagnetism.Dynamics.Basic
+module
+
+public import PhysLean.Electromagnetism.Kinematics.MagneticField
+public import PhysLean.Electromagnetism.Dynamics.Basic
/-!
# The kinetic term
@@ -58,6 +60,8 @@ In this implementation we have set `μ₀ = 1`. It is a TODO to introduce this c
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Dynamics/Lagrangian.lean b/PhysLean/Electromagnetism/Dynamics/Lagrangian.lean
index d4219ab6b..1b21f1fae 100644
--- a/PhysLean/Electromagnetism/Dynamics/Lagrangian.lean
+++ b/PhysLean/Electromagnetism/Dynamics/Lagrangian.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.CurrentDensity
-import PhysLean.Electromagnetism.Dynamics.KineticTerm
+module
+
+public import PhysLean.Electromagnetism.Dynamics.CurrentDensity
+public import PhysLean.Electromagnetism.Dynamics.KineticTerm
/-!
# The Lagrangian in electromagnetism
@@ -62,6 +64,8 @@ In this implementation we set `μ₀ = 1`. It is a TODO to introduce this consta
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Kinematics/Boosts.lean b/PhysLean/Electromagnetism/Kinematics/Boosts.lean
index 12db3e0eb..f6b367834 100644
--- a/PhysLean/Electromagnetism/Kinematics/Boosts.lean
+++ b/PhysLean/Electromagnetism/Kinematics/Boosts.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.MagneticField
-import PhysLean.SpaceAndTime.SpaceTime.Boosts
+module
+
+public import PhysLean.Electromagnetism.Kinematics.MagneticField
+public import PhysLean.SpaceAndTime.SpaceTime.Boosts
/-!
# Boosts on the electric and magnetic fields
@@ -41,6 +43,8 @@ See e.g.
-/
+@[expose] public section
+
namespace Electromagnetism
namespace ElectromagneticPotential
diff --git a/PhysLean/Electromagnetism/Kinematics/EMPotential.lean b/PhysLean/Electromagnetism/Kinematics/EMPotential.lean
index f76046a36..f0239b1f1 100644
--- a/PhysLean/Electromagnetism/Kinematics/EMPotential.lean
+++ b/PhysLean/Electromagnetism/Kinematics/EMPotential.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Basic
-import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Electromagnetism.Basic
+public import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
/-!
# The Electromagnetic Potential
@@ -47,6 +49,8 @@ spacetime to contravariant Lorentz vectors.
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Kinematics/ElectricField.lean b/PhysLean/Electromagnetism/Kinematics/ElectricField.lean
index 9a9024a88..566da2ff6 100644
--- a/PhysLean/Electromagnetism/Kinematics/ElectricField.lean
+++ b/PhysLean/Electromagnetism/Kinematics/ElectricField.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.VectorPotential
-import PhysLean.Electromagnetism.Kinematics.ScalarPotential
-import PhysLean.Electromagnetism.Kinematics.FieldStrength
+module
+
+public import PhysLean.Electromagnetism.Kinematics.VectorPotential
+public import PhysLean.Electromagnetism.Kinematics.ScalarPotential
+public import PhysLean.Electromagnetism.Kinematics.FieldStrength
/-!
# The Electric Field
@@ -38,6 +40,8 @@ In this module we define the electric field, and prove lemmas about it.
## iv. References
-/
+
+@[expose] public section
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Kinematics/FieldStrength.lean b/PhysLean/Electromagnetism/Kinematics/FieldStrength.lean
index c091859ee..e7b873476 100644
--- a/PhysLean/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/PhysLean/Electromagnetism/Kinematics/FieldStrength.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.EMPotential
+module
+
+public import PhysLean.Electromagnetism.Kinematics.EMPotential
/-!
# The Field Strength Tensor
@@ -41,6 +43,8 @@ We define a tensor version and a matrix version and prover various properties of
## iv. References
-/
+
+@[expose] public section
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Kinematics/MagneticField.lean b/PhysLean/Electromagnetism/Kinematics/MagneticField.lean
index db43e67c5..d2d65ebfa 100644
--- a/PhysLean/Electromagnetism/Kinematics/MagneticField.lean
+++ b/PhysLean/Electromagnetism/Kinematics/MagneticField.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.ElectricField
+module
+
+public import PhysLean.Electromagnetism.Kinematics.ElectricField
/-!
# The Magnetic Field
@@ -50,6 +52,8 @@ field strength matrix. This is an antisymmetric matrix.
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean b/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean
index 6d4a3f722..33cdd1a52 100644
--- a/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean
+++ b/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.EMPotential
+module
+
+public import PhysLean.Electromagnetism.Kinematics.EMPotential
/-!
# The Scalar Potential
@@ -36,6 +38,8 @@ the scalar potential is non-relativistic and is therefore a function of `Time` a
## iv. References
-/
+
+@[expose] public section
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean b/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean
index d8cb943d9..ebbe360a8 100644
--- a/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean
+++ b/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Kinematics.EMPotential
+module
+
+public import PhysLean.Electromagnetism.Kinematics.EMPotential
/-!
# The vector Potential
@@ -37,6 +39,8 @@ the vector potential is non-relativistic and is therefore a function of `Time` a
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/PointParticle/OneDimension.lean b/PhysLean/Electromagnetism/PointParticle/OneDimension.lean
index e8f72a743..03a16079d 100644
--- a/PhysLean/Electromagnetism/PointParticle/OneDimension.lean
+++ b/PhysLean/Electromagnetism/PointParticle/OneDimension.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
-import PhysLean.SpaceAndTime.Space.Norm
-import PhysLean.SpaceAndTime.Space.Translations
-import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
+module
+
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
+public import PhysLean.SpaceAndTime.Space.Norm
+public import PhysLean.SpaceAndTime.Space.Translations
+public import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
/-!
# The electrostatics of a stationary point particle in 1d
@@ -39,6 +41,8 @@ sitting at the origin in 1d space.
-/
+@[expose] public section
+
namespace Electromagnetism
open Distribution SchwartzMap
open Space MeasureTheory
diff --git a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
index 301024f24..107c34a5f 100644
--- a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
+++ b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
-import PhysLean.SpaceAndTime.Space.Norm
-import PhysLean.SpaceAndTime.Space.Translations
-import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
+module
+
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
+public import PhysLean.SpaceAndTime.Space.Norm
+public import PhysLean.SpaceAndTime.Space.Translations
+public import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
/-!
# Electrostatics of a stationary point particle in 3d
@@ -41,6 +43,8 @@ sitting at the origin in 3d space.
-/
+@[expose] public section
+
namespace Electromagnetism
open Distribution SchwartzMap
open Space MeasureTheory
diff --git a/PhysLean/Electromagnetism/Vacuum/Constant.lean b/PhysLean/Electromagnetism/Vacuum/Constant.lean
index fe943b1c8..8b7b3a582 100644
--- a/PhysLean/Electromagnetism/Vacuum/Constant.lean
+++ b/PhysLean/Electromagnetism/Vacuum/Constant.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
+module
+
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
/-!
# The constant electric and magnetic fields
@@ -34,6 +36,8 @@ electromagnetic action.
-/
+@[expose] public section
+
namespace Electromagnetism
open Module realLorentzTensor
open IndexNotation
diff --git a/PhysLean/Electromagnetism/Vacuum/HarmonicWave.lean b/PhysLean/Electromagnetism/Vacuum/HarmonicWave.lean
index e3fca392b..b5d9b779a 100644
--- a/PhysLean/Electromagnetism/Vacuum/HarmonicWave.lean
+++ b/PhysLean/Electromagnetism/Vacuum/HarmonicWave.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Joseph Tooby-Smith
-/
-import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
+module
+
+public import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
/-!
# Harmonic Wave in Vacuum
@@ -49,6 +51,8 @@ form of a matrix rather than a vector.
## iv. References
-/
+
+@[expose] public section
namespace Electromagnetism
open Space Module
diff --git a/PhysLean/Electromagnetism/Vacuum/IsPlaneWave.lean b/PhysLean/Electromagnetism/Vacuum/IsPlaneWave.lean
index 7f2e4b920..0c70be227 100644
--- a/PhysLean/Electromagnetism/Vacuum/IsPlaneWave.lean
+++ b/PhysLean/Electromagnetism/Vacuum/IsPlaneWave.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Joseph Tooby-Smith
-/
-import PhysLean.ClassicalMechanics.WaveEquation.Basic
-import PhysLean.Electromagnetism.Dynamics.IsExtrema
+module
+
+public import PhysLean.ClassicalMechanics.WaveEquation.Basic
+public import PhysLean.Electromagnetism.Dynamics.IsExtrema
/-!
# Electromagnetic wave equation
@@ -51,6 +53,8 @@ in general dimensions.
-/
+@[expose] public section
+
namespace Electromagnetism
open Space Module
diff --git a/PhysLean/Mathematics/Calculus/AdjFDeriv.lean b/PhysLean/Mathematics/Calculus/AdjFDeriv.lean
index 8a9f5aedf..733dba9c2 100644
--- a/PhysLean/Mathematics/Calculus/AdjFDeriv.lean
+++ b/PhysLean/Mathematics/Calculus/AdjFDeriv.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
-import Mathlib.Analysis.Calculus.Gradient.Basic
-import PhysLean.Mathematics.FDerivCurry
-import PhysLean.Mathematics.InnerProductSpace.Adjoint
-import PhysLean.Mathematics.InnerProductSpace.Calculus
+module
+
+public import Mathlib.Analysis.Calculus.Gradient.Basic
+public import PhysLean.Mathematics.FDerivCurry
+public import PhysLean.Mathematics.InnerProductSpace.Adjoint
+public import PhysLean.Mathematics.InnerProductSpace.Calculus
/-!
# Adjoint Fréchet derivative
@@ -24,6 +26,8 @@ the natural product is `WithLp 2 (X × Y)`.
For example:
-/
+@[expose] public section
+
noncomputable section
variable
diff --git a/PhysLean/Mathematics/Calculus/Divergence.lean b/PhysLean/Mathematics/Calculus/Divergence.lean
index 4547076c5..b909940b7 100644
--- a/PhysLean/Mathematics/Calculus/Divergence.lean
+++ b/PhysLean/Mathematics/Calculus/Divergence.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
-import Mathlib.Analysis.InnerProductSpace.Trace
-import PhysLean.Mathematics.Calculus.AdjFDeriv
-import PhysLean.SpaceAndTime.TimeAndSpace.Basic
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Trace
+public import PhysLean.Mathematics.Calculus.AdjFDeriv
+public import PhysLean.SpaceAndTime.TimeAndSpace.Basic
/-!
# Divergence
@@ -14,6 +16,8 @@ In this module we define and create an API around the divergence of a map `f : E
where `E` is a normed space over a field `𝕜`.
-/
+
+@[expose] public section
noncomputable section
open Module
open scoped InnerProductSpace
diff --git a/PhysLean/Mathematics/DataStructures/FourTree/Basic.lean b/PhysLean/Mathematics/DataStructures/FourTree/Basic.lean
index 528c2c3ea..f4a0a6d5d 100644
--- a/PhysLean/Mathematics/DataStructures/FourTree/Basic.lean
+++ b/PhysLean/Mathematics/DataStructures/FourTree/Basic.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Data.Multiset.Bind
-import Mathlib.Data.Multiset.Sort
+module
+
+public import Mathlib.Data.Multiset.Bind
+public import Mathlib.Data.Multiset.Sort
/-!
## The data type FourTree
@@ -21,6 +23,8 @@ It is defined recursively, with the following structure:
-/
+@[expose] public section
+
namespace PhysLean
namespace FourTree
diff --git a/PhysLean/Mathematics/DataStructures/FourTree/UniqueMap.lean b/PhysLean/Mathematics/DataStructures/FourTree/UniqueMap.lean
index 3b80d890e..5880748af 100644
--- a/PhysLean/Mathematics/DataStructures/FourTree/UniqueMap.lean
+++ b/PhysLean/Mathematics/DataStructures/FourTree/UniqueMap.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.DataStructures.FourTree.Basic
+module
+
+public import PhysLean.Mathematics.DataStructures.FourTree.Basic
/-!
## Unique maps for `FourTree`
@@ -15,6 +17,8 @@ the tree has no duplicates).
-/
+@[expose] public section
+
namespace PhysLean
namespace FourTree
diff --git a/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean b/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean
index 31878cf68..f0afce04d 100644
--- a/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean
+++ b/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Matteo Cipollina. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina
-/
-import Mathlib.Analysis.Complex.Polynomial.Basic
-import Mathlib.Analysis.Normed.Algebra.MatrixExponential
-import PhysLean.Mathematics.SchurTriangulation
+module
+
+public import Mathlib.Analysis.Complex.Polynomial.Basic
+public import Mathlib.Analysis.Normed.Algebra.MatrixExponential
+public import PhysLean.Mathematics.SchurTriangulation
/-!
# Lie's Trace Formula
@@ -22,6 +24,8 @@ is defined in `mathlib` as `Matrix.BlockTriangular A id`.
- `Matrix.det_exp`: The determinant of the exponential of a matrix is the exponential of its trace.
-/
+@[expose] public section
+
namespace Matrix
open scoped BigOperators Topology
diff --git a/PhysLean/Mathematics/Distribution/Basic.lean b/PhysLean/Mathematics/Distribution/Basic.lean
index 76db930e2..069366d6f 100644
--- a/PhysLean/Mathematics/Distribution/Basic.lean
+++ b/PhysLean/Mathematics/Distribution/Basic.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Joseph Tooby-Smith
-/
-import Mathlib.Analysis.Distribution.TemperedDistribution
-import PhysLean.Meta.TODO.Basic
+module
+
+public import Mathlib.Analysis.Distribution.TemperedDistribution
+public import PhysLean.Meta.TODO.Basic
/-!
# Distributions
@@ -39,6 +41,8 @@ functions from `E` to `F`. We give a more precise definition of distributions be
-/
+@[expose] public section
+
open SchwartzMap NNReal
noncomputable section
diff --git a/PhysLean/Mathematics/Distribution/PowMul.lean b/PhysLean/Mathematics/Distribution/PowMul.lean
index 25e74f8c3..718eef0b7 100644
--- a/PhysLean/Mathematics/Distribution/PowMul.lean
+++ b/PhysLean/Mathematics/Distribution/PowMul.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.Distribution.Basic
-import Mathlib.MeasureTheory.Constructions.HaarToSphere
+module
+
+public import PhysLean.Mathematics.Distribution.Basic
+public import Mathlib.MeasureTheory.Constructions.HaarToSphere
/-!
## The multiple of a Schwartz map by `x`
@@ -13,6 +15,8 @@ In this module we define the continuous linear map from the Schwartz space
`𝓢(ℝ, 𝕜)` to itself which takes a Schwartz map `η` to the Schwartz map `x * η`.
-/
+
+@[expose] public section
open SchwartzMap NNReal
noncomputable section
@@ -24,7 +28,7 @@ variable [NormedSpace ℝ E]
open ContDiff
open MeasureTheory
-private lemma norm_iteratedFDeriv_ofRealCLM {x} (i : ℕ) :
+lemma norm_iteratedFDeriv_ofRealCLM {x} (i : ℕ) :
‖iteratedFDeriv ℝ i (RCLike.ofRealCLM (K := 𝕜)) x‖ =
if i = 0 then |x| else if i = 1 then 1 else 0 := by
match i with
@@ -112,7 +116,7 @@ def powOneMul : 𝓢(ℝ, 𝕜) →L[𝕜] 𝓢(ℝ, 𝕜) := by
zero_mul, Finset.sum_singleton, ↓reduceIte, Nat.choose_self, Nat.cast_one, one_mul,
Nat.sub_zero, norm_iteratedFDeriv_zero, CharP.cast_eq_zero, ge_iff_le]
trans (SchwartzMap.seminorm 𝕜 (k + 1) 0) ψ
- · apply le_trans ?_ (ψ.le_seminorm ℝ _ _ x)
+ · apply le_trans ?_ (ψ.le_seminorm 𝕜 _ _ x)
simp only [Real.norm_eq_abs, norm_iteratedFDeriv_zero]
ring_nf
rfl
@@ -135,8 +139,8 @@ def powOneMul : 𝓢(ℝ, 𝕜) →L[𝕜] 𝓢(ℝ, 𝕜) := by
refine Left.add_nonneg ?_ ?_
· exact Nat.cast_nonneg' n
· exact zero_le_one' ℝ
- · exact ψ.le_seminorm ℝ k n x
- · exact ψ.le_seminorm ℝ (k + 1) (n + 1) x
+ · exact ψ.le_seminorm 𝕜 k n x
+ · exact ψ.le_seminorm 𝕜 (k + 1) (n + 1) x
· by_cases h1 :((SchwartzMap.seminorm 𝕜 (k + 1) (n + 1)) ψ) <
((SchwartzMap.seminorm 𝕜 k n) ψ)
· rw [max_eq_left_of_lt h1]
diff --git a/PhysLean/Mathematics/FDerivCurry.lean b/PhysLean/Mathematics/FDerivCurry.lean
index bc2ed0359..6d1f6373f 100644
--- a/PhysLean/Mathematics/FDerivCurry.lean
+++ b/PhysLean/Mathematics/FDerivCurry.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Tomáš Skřivan, Joseph Tooby-Smith
-/
-import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+module
+
+public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-!
# fderiv currying lemmas
Various lemmas related to fderiv on curried/uncurried functions.
-/
+
+@[expose] public section
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
{X Y Z : Type*} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
[NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
diff --git a/PhysLean/Mathematics/Fin.lean b/PhysLean/Mathematics/Fin.lean
index 045506a32..26b6e8c13 100644
--- a/PhysLean/Mathematics/Fin.lean
+++ b/PhysLean/Mathematics/Fin.lean
@@ -3,9 +3,11 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Tactic.Polyrith
-import Mathlib.Tactic.Linarith
-import Mathlib.Logic.Equiv.Fin.Basic
+module
+
+public import Mathlib.Tactic.Polyrith
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Logic.Equiv.Fin.Basic
/-!
# Fin lemmas
@@ -16,6 +18,8 @@ At some point these should either be up-streamed to Mathlib or replaced with def
in Mathlib.
-/
+
+@[expose] public section
namespace PhysLean.Fin
open Fin
diff --git a/PhysLean/Mathematics/Fin/Involutions.lean b/PhysLean/Mathematics/Fin/Involutions.lean
index 905e6a9db..e4cb60366 100644
--- a/PhysLean/Mathematics/Fin/Involutions.lean
+++ b/PhysLean/Mathematics/Fin/Involutions.lean
@@ -3,12 +3,14 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Tactic.Polyrith
-import Mathlib.Tactic.Linarith
-import Mathlib.Data.Nat.Factorial.DoubleFactorial
-import Mathlib.Data.Finset.Sort
-import Mathlib.Data.Fintype.Pi
-import Mathlib.Data.Fintype.Prod
+module
+
+public import Mathlib.Tactic.Polyrith
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Data.Nat.Factorial.DoubleFactorial
+public import Mathlib.Data.Finset.Sort
+public import Mathlib.Data.Fintype.Pi
+public import Mathlib.Data.Fintype.Prod
/-!
# Fin involutions
@@ -17,6 +19,8 @@ Some properties of involutions of `Fin n`.
These involutions are used in e.g. proving results about Wick contractions.
-/
+
+@[expose] public section
namespace PhysLean.Fin
open Nat
diff --git a/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
index c5a120a0d..0aabad9ad 100644
--- a/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
+++ b/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
@@ -3,13 +3,14 @@ Copyright (c) 2025 Matteo Cipollina. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina
-/
+module
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.RCLike.Lemmas
-import Mathlib.Geometry.Manifold.MFDeriv.Defs
-import Mathlib.LinearAlgebra.BilinearForm.Properties
-import Mathlib.LinearAlgebra.QuadraticForm.Real
-import Mathlib.Topology.LocallyConstant.Basic
+public import Mathlib.Analysis.InnerProductSpace.Basic
+public import Mathlib.Analysis.RCLike.Lemmas
+public import Mathlib.Geometry.Manifold.MFDeriv.Defs
+public import Mathlib.LinearAlgebra.BilinearForm.Properties
+public import Mathlib.LinearAlgebra.QuadraticForm.Real
+public import Mathlib.Topology.LocallyConstant.Basic
/-!
# Pseudo-Riemannian Metrics on Smooth Manifolds
@@ -51,6 +52,8 @@ sections of a tensor bundle (e.g., `Hom(TM ⊗ TM, ℝ)` or `TM →L[ℝ] TM →
leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.28Pseudo.29.20Riemannian.20metric
-/
+@[expose] public section
+
section PseudoRiemannianMetric
noncomputable section
@@ -184,7 +187,7 @@ The quadratic form `Qₓ` at `x` is defined as `Qₓ(v) = gₓ(v,v)`.
The associated symmetric bilinear form required by `QuadraticForm.exists_companion'`
is `Bₓ(v,w) = gₓ(v,w) + gₓ(w,v)`. Given the symmetry `symm`, this is `2 * gₓ(v,w)`.
-/
-private def pseudoRiemannianMetricValToQuadraticForm
+def pseudoRiemannianMetricValToQuadraticForm
{E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E]
{H : Type w} [TopologicalSpace H]
{M : Type w} [TopologicalSpace M] [ChartedSpace H M]
diff --git a/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean b/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean
index 3caa55842..a79bcf5c1 100644
--- a/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean
+++ b/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean
@@ -3,15 +3,19 @@ Copyright (c) 2025 Matteo Cipollina. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina
-/
-import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
-import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
+module
+
+public import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
+public import Mathlib.Algebra.Lie.OfAssociative
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-!
# Riemannian Metric Definitions
This module defines the Riemannian metric, building on pseudo-Riemannian metrics.
-/
+@[expose] public section
+
namespace PseudoRiemannianMetric
section RiemannianMetric
diff --git a/PhysLean/Mathematics/InnerProductSpace/Adjoint.lean b/PhysLean/Mathematics/InnerProductSpace/Adjoint.lean
index ffb352a91..53393b50f 100644
--- a/PhysLean/Mathematics/InnerProductSpace/Adjoint.lean
+++ b/PhysLean/Mathematics/InnerProductSpace/Adjoint.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
-import PhysLean.Mathematics.InnerProductSpace.Basic
-import Mathlib.Analysis.InnerProductSpace.Adjoint
+module
+
+public import PhysLean.Mathematics.InnerProductSpace.Basic
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
/-!
# Adjoint of a linear map
@@ -16,6 +18,8 @@ This is a generalization of the usual adjoint defined on `InnerProductSpace` for
continuous linear maps.
-/
+
+@[expose] public section
variable {𝕜 : Type*} {E F G : Type*} [RCLike 𝕜]
[NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E]
[NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F]
diff --git a/PhysLean/Mathematics/InnerProductSpace/Basic.lean b/PhysLean/Mathematics/InnerProductSpace/Basic.lean
index bef7b3863..e94abc7ba 100644
--- a/PhysLean/Mathematics/InnerProductSpace/Basic.lean
+++ b/PhysLean/Mathematics/InnerProductSpace/Basic.lean
@@ -3,11 +3,13 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
-import Mathlib.Analysis.InnerProductSpace.Calculus
-import Mathlib.Analysis.InnerProductSpace.Completion
-import Mathlib.Analysis.InnerProductSpace.ProdL2
-import Mathlib.Data.Real.CompleteField
-import Mathlib.Data.Real.StarOrdered
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Calculus
+public import Mathlib.Analysis.InnerProductSpace.Completion
+public import Mathlib.Analysis.InnerProductSpace.ProdL2
+public import Mathlib.Data.Real.CompleteField
+public import Mathlib.Data.Real.StarOrdered
/-!
# Inner product space
@@ -28,6 +30,8 @@ We define the following maps:
-/
+@[expose] public section
+
/-- L₂ norm on `E`.
In particular, on product types `X×Y` and pi types `ι → X` this class provides L₂ norm unlike `‖·‖`.
diff --git a/PhysLean/Mathematics/InnerProductSpace/Calculus.lean b/PhysLean/Mathematics/InnerProductSpace/Calculus.lean
index 9b5b168d2..282c85c0a 100644
--- a/PhysLean/Mathematics/InnerProductSpace/Calculus.lean
+++ b/PhysLean/Mathematics/InnerProductSpace/Calculus.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
-import PhysLean.Mathematics.InnerProductSpace.Basic
-import Mathlib.Analysis.InnerProductSpace.Adjoint
+module
+
+public import PhysLean.Mathematics.InnerProductSpace.Basic
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
/-!
# Generalization of calculus results to `InnerProductSpace'`
-/
+
+@[expose] public section
variable {𝕜 : Type*} {E F G : Type*} [RCLike 𝕜]
[NormedAddCommGroup E] [NormedSpace ℝ E]
[NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace' ℝ F]
diff --git a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean
index 452258608..3a7a7dbc5 100644
--- a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean
+++ b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean
@@ -3,7 +3,9 @@ Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
-import Mathlib.Analysis.InnerProductSpace.LinearPMap
+module
+
+public import Mathlib.Analysis.InnerProductSpace.LinearPMap
/-!
# Submodules of `E × E`
@@ -15,6 +17,8 @@ by default `E × E` is given the sup norm.
-/
+@[expose] public section
+
namespace InnerProductSpaceSubmodule
open LinearPMap Submodule
diff --git a/PhysLean/Mathematics/KroneckerDelta.lean b/PhysLean/Mathematics/KroneckerDelta.lean
index 448a6e026..5a935b36c 100644
--- a/PhysLean/Mathematics/KroneckerDelta.lean
+++ b/PhysLean/Mathematics/KroneckerDelta.lean
@@ -3,8 +3,10 @@ Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
-import Mathlib.Algebra.Ring.Basic
-import PhysLean.Meta.TODO.Basic
+module
+
+public import Mathlib.Algebra.Ring.Basic
+public import PhysLean.Meta.TODO.Basic
/-!
# Kronecker delta
@@ -12,6 +14,8 @@ import PhysLean.Meta.TODO.Basic
This file defines the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`.
-/
+
+@[expose] public section
TODO "YVABB" "Build functionality for working with sums involving Kronecker deltas."
namespace KroneckerDelta
diff --git a/PhysLean/Mathematics/LinearMaps.lean b/PhysLean/Mathematics/LinearMaps.lean
index 7c32ea911..397fc494d 100644
--- a/PhysLean/Mathematics/LinearMaps.lean
+++ b/PhysLean/Mathematics/LinearMaps.lean
@@ -3,11 +3,13 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Tactic.Polyrith
-import Mathlib.Algebra.Module.LinearMap.Defs
-import Mathlib.Data.Fintype.BigOperators
-import PhysLean.Meta.TODO.Basic
-import Mathlib.Algebra.Ring.Rat
+module
+
+public import Mathlib.Tactic.Polyrith
+public import Mathlib.Algebra.Module.LinearMap.Defs
+public import Mathlib.Data.Fintype.BigOperators
+public import PhysLean.Meta.TODO.Basic
+public import Mathlib.Algebra.Ring.Rat
/-!
# Linear maps
@@ -15,6 +17,8 @@ Some definitions and properties of linear, bilinear, and trilinear maps, along w
quadratic and cubic equations.
-/
+
+@[expose] public section
TODO "6VZLZ" "Replace the definitions in this file with Mathlib definitions."
/-- The structure defining a homogeneous quadratic equation. -/
diff --git a/PhysLean/Mathematics/List.lean b/PhysLean/Mathematics/List.lean
index 3781a13b2..d92050c26 100644
--- a/PhysLean/Mathematics/List.lean
+++ b/PhysLean/Mathematics/List.lean
@@ -3,13 +3,18 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.Fin
-import Mathlib.Data.Nat.Lattice
-import Mathlib.Data.List.TakeWhile
+module
+public import PhysLean.Mathematics.Fin
+public import Mathlib.Data.Nat.Lattice
+public import Mathlib.Data.List.TakeWhile
+import all Mathlib.Data.List.Sort
+public import Mathlib.Logic.Equiv.Defs
/-!
# List lemmas
-/
+public section
+
namespace PhysLean.List
open Fin
@@ -128,6 +133,7 @@ lemma insertionSort_length {I : Type} (le1 : I → I → Prop) [DecidableRel le1
List.Perm.length_eq (List.perm_insertionSort le1 l)
/-- The position `r0` ends up in `r` on adding it via `List.orderedInsert _ r0 r`. -/
+@[expose]
def orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
Fin (List.orderedInsert le1 r0 r).length :=
⟨(List.takeWhile (fun b => decide ¬ le1 r0 b) r).length, by
@@ -341,6 +347,7 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
/-- The equivalence between `Fin (r0 :: r).length` and `Fin (List.orderedInsert le1 r0 r).length`
according to where the elements map, i.e. `0` is taken to `orderedInsertPos le1 r r0`. -/
+@[expose]
def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length := by
let e2 : Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length :=
@@ -639,7 +646,7 @@ lemma insertionSortEquiv_order {α : Type} {r : α → α → Prop} [DecidableRe
/-- Optional erase of an element in a list. For `none` returns the list, for `some i` returns
the list with the `i`'th element erased. -/
-def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
+@[expose] def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
match i with
| none => l
| some i => List.eraseIdx l i
@@ -721,13 +728,14 @@ lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableR
of `l` such that for every element `(i :: l)[b]` before that position
`r ((i :: l)[b]) ((i :: l)[a])` is not true. The use of `i :: l` here
rather then just `l` is to ensure that such a position exists. . -/
+@[expose]
def insertionSortMinPos {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) :
Fin (i :: l).length := (insertionSortEquiv r (i :: l)).symm ⟨0, by
rw [insertionSort_length]
exact Nat.zero_lt_succ l.length⟩
/-- The element of `i :: l` at `insertionSortMinPos`. -/
-def insertionSortMin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) :
+@[expose] def insertionSortMin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) :
α := (i :: l).get (insertionSortMinPos r i l)
lemma insertionSortMin_eq_insertionSort_head {α : Type} (r : α → α → Prop) [DecidableRel r]
@@ -746,6 +754,7 @@ lemma insertionSortMin_eq_insertionSort_head {α : Type} (r : α → α → Prop
/-- The list remaining after dropping the element at the position determined by
`insertionSortMinPos`. -/
+@[expose]
def insertionSortDropMinPos {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) :
List α := (i :: l).eraseIdx (insertionSortMinPos r i l)
@@ -766,7 +775,7 @@ lemma insertionSort_eq_insertionSortMin_cons {α : Type} (r : α → α → Prop
front of the list, for `some i` removes the `i`th element of the list (does not add `a`).
E.g. `optionEraseZ [0, 1, 2] 4 none = [4, 0, 1, 2]` and
`optionEraseZ [0, 1, 2] 4 (some 1) = [0, 2]`. -/
-def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I :=
+@[expose] def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I :=
match i with
| none => a :: l
| some i => List.eraseIdx l i
diff --git a/PhysLean/Mathematics/List/InsertIdx.lean b/PhysLean/Mathematics/List/InsertIdx.lean
index 399af0cb5..491eb6ba5 100644
--- a/PhysLean/Mathematics/List/InsertIdx.lean
+++ b/PhysLean/Mathematics/List/InsertIdx.lean
@@ -3,12 +3,16 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Data.List.Sort
-import Mathlib.Algebra.Order.Ring.Nat
+module
+
+public import Mathlib.Data.List.Sort
+public import Mathlib.Algebra.Order.Ring.Nat
/-!
# List lemmas
-/
+
+@[expose] public section
namespace PhysLean.List
open Fin
diff --git a/PhysLean/Mathematics/List/InsertionSort.lean b/PhysLean/Mathematics/List/InsertionSort.lean
index 97310421f..ce505a5ca 100644
--- a/PhysLean/Mathematics/List/InsertionSort.lean
+++ b/PhysLean/Mathematics/List/InsertionSort.lean
@@ -3,11 +3,17 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.List
+module
+public import PhysLean.Mathematics.List
+import all PhysLean.Mathematics.List
+import all Mathlib.Data.List.Sort
/-!
# List lemmas
-/
+
+@[expose] public section
+
namespace PhysLean.List
open Fin
diff --git a/PhysLean/Mathematics/PiTensorProduct.lean b/PhysLean/Mathematics/PiTensorProduct.lean
index 9a0c2b3f7..b5d23bd96 100644
--- a/PhysLean/Mathematics/PiTensorProduct.lean
+++ b/PhysLean/Mathematics/PiTensorProduct.lean
@@ -3,7 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.LinearAlgebra.PiTensorProduct
+module
+
+public import Mathlib.LinearAlgebra.PiTensorProduct
/-!
# Pi Tensor Products
@@ -14,6 +16,8 @@ At some point these should either be up-streamed to Mathlib or replaced with def
in Mathlib.
-/
+
+@[expose] public section
namespace PhysLean.PiTensorProduct
noncomputable section tmulEquiv
diff --git a/PhysLean/Mathematics/RatComplexNum.lean b/PhysLean/Mathematics/RatComplexNum.lean
index a60362dfc..ab5dbf63b 100644
--- a/PhysLean/Mathematics/RatComplexNum.lean
+++ b/PhysLean/Mathematics/RatComplexNum.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Analysis.Complex.Basic
+module
+
+public import Mathlib.Analysis.Complex.Basic
/-!
# Rational complex numbers
-/
+@[expose] public section
+
namespace PhysLean
/-- Rational complex numbers. This type is mainly used when decidability is needed. -/
diff --git a/PhysLean/Mathematics/SO3/Basic.lean b/PhysLean/Mathematics/SO3/Basic.lean
index f2e3f9406..6527a88cf 100644
--- a/PhysLean/Mathematics/SO3/Basic.lean
+++ b/PhysLean/Mathematics/SO3/Basic.lean
@@ -3,13 +3,17 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.LinearAlgebra.Eigenspace.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
+module
+
+public import Mathlib.LinearAlgebra.Eigenspace.Basic
+public import Mathlib.Analysis.InnerProductSpace.PiL2
/-!
# The group SO(3)
-/
+@[expose] public section
+
namespace GroupTheory
open Matrix
diff --git a/PhysLean/Mathematics/SchurTriangulation.lean b/PhysLean/Mathematics/SchurTriangulation.lean
index 81eb6c360..9bc50b402 100644
--- a/PhysLean/Mathematics/SchurTriangulation.lean
+++ b/PhysLean/Mathematics/SchurTriangulation.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Gordon Hsu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gordon Hsu
-/
-import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
-import Mathlib.Analysis.InnerProductSpace.Adjoint
+module
+
+public import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
/-! # Schur triangulation
Schur triangulation is more commonly known as Schur decomposition or Schur triangularization, but
@@ -22,6 +24,8 @@ be decomposed as `A = U * T * star U` where `U` is unitary and `T` is upper tria
-/
+@[expose] public section
+
open scoped InnerProductSpace
open Module
@@ -235,7 +239,7 @@ variable [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrd
/-- This is `LinearMap.SchurTriangulationAux` adapted for matrices in the
Euclidean space. -/
-private noncomputable def schurTriangulationAux :
+noncomputable def schurTriangulationAux :
OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n) × UpperTriangular n 𝕜 :=
let f := toEuclideanLin A
let ⟨d, hd, b, hut⟩ := LinearMap.SchurTriangulationAux.of f
diff --git a/PhysLean/Mathematics/SpecialFunctions/PhysHermite.lean b/PhysLean/Mathematics/SpecialFunctions/PhysHermite.lean
index 60f13af7e..ca17d38ea 100644
--- a/PhysLean/Mathematics/SpecialFunctions/PhysHermite.lean
+++ b/PhysLean/Mathematics/SpecialFunctions/PhysHermite.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import Mathlib.Analysis.Calculus.Deriv.Polynomial
-import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
-import Mathlib.Tactic.Cases
+module
+
+public import Mathlib.Analysis.Calculus.Deriv.Polynomial
+public import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
+public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
+public import Mathlib.Tactic.Cases
/-!
# Physicists Hermite Polynomial
@@ -15,6 +17,8 @@ This file may eventually be upstreamed to Mathlib.
-/
+@[expose] public section
+
open Polynomial
namespace PhysLean
diff --git a/PhysLean/Mathematics/Trigonometry/Tanh.lean b/PhysLean/Mathematics/Trigonometry/Tanh.lean
index 7a1e87a42..ca52f89d0 100644
--- a/PhysLean/Mathematics/Trigonometry/Tanh.lean
+++ b/PhysLean/Mathematics/Trigonometry/Tanh.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Afiq Hatta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Afiq Hatta
-/
-import Mathlib.Topology.Algebra.Polynomial
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
-import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
+module
+
+public import Mathlib.Topology.Algebra.Polynomial
+public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
+public import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-!
# Properties of Tanh
We want to prove that the reflectionless potential is a Schwartz map.
@@ -18,6 +20,8 @@ the nth derivative of a function multiplied by tanh decays faster than any polyn
- Fill in the proofs for the properties of tanh
-/
+@[expose] public section
+
open Real
open NNReal
open Field
diff --git a/PhysLean/Mathematics/VariationalCalculus/Basic.lean b/PhysLean/Mathematics/VariationalCalculus/Basic.lean
index 497c38b2d..cdba4955a 100644
--- a/PhysLean/Mathematics/VariationalCalculus/Basic.lean
+++ b/PhysLean/Mathematics/VariationalCalculus/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
/-!
# Fundamental lemma of the calculus of variations
@@ -16,6 +18,8 @@ which allows use to go from reasoning about integrals to reasoning about functio
-/
+@[expose] public section
+
open MeasureTheory InnerProductSpace InnerProductSpace'
variable
diff --git a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean b/PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean
index 0b9c25e6d..c62ad81f1 100644
--- a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean
+++ b/PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
/-!
# Variational adjoint derivative
@@ -20,6 +22,8 @@ theorem saying
This theorem is the main tool to mechanistically compute variational gradient.
-/
+@[expose] public section
+
open MeasureTheory ContDiff InnerProductSpace
variable
diff --git a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean b/PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean
index f596c544f..19f86fa1b 100644
--- a/PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean
+++ b/PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
/-!
# Variational adjoint
@@ -23,6 +25,8 @@ The key results are:
`HasVarAdjoint.mul_right`, `HasVarAdjoint.smul_left`, `HasVarAdjoint.smul_right`
-/
+@[expose] public section
+
open Module InnerProductSpace MeasureTheory ContDiff
variable
diff --git a/PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean b/PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean
index fea9015dd..b9dfa00bc 100644
--- a/PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean
+++ b/PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
/-!
# Variational gradient
@@ -12,6 +14,8 @@ Definition of variational gradient that allows for formal treatment of variation
as used in physics textbooks.
-/
+@[expose] public section
+
open MeasureTheory ContDiff InnerProductSpace
variable
diff --git a/PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean b/PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean
index cb2e48f5f..479fa55c9 100644
--- a/PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean
+++ b/PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.VariationalCalculus.Basic
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.Basic
/-!
# Localized function transforms
@@ -14,6 +16,8 @@ set `K` in `Y` there exists a compact set `L` of `X`, such that if `φ` and `φ'
then `F φ` and `F φ'` are equal on `K`.
-/
+
+@[expose] public section
open InnerProductSpace MeasureTheory ContDiff
section
diff --git a/PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean b/PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean
index 8b21454c0..a8084e128 100644
--- a/PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean
+++ b/PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
-import PhysLean.Mathematics.Calculus.Divergence
+module
+
+public import PhysLean.Mathematics.Calculus.Divergence
/-!
# Test functions
Definition of test function, smooth and compactly supported function, and theorems about them.
-/
+
+@[expose] public section
open Module
section IsTestFunction
variable
diff --git a/PhysLean/Meta/AllFilePaths.lean b/PhysLean/Meta/AllFilePaths.lean
index 634f41974..673e1f2ff 100644
--- a/PhysLean/Meta/AllFilePaths.lean
+++ b/PhysLean/Meta/AllFilePaths.lean
@@ -3,13 +3,17 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.TODO.Basic
+module
+
+public import PhysLean.Meta.TODO.Basic
/-!
## Getting an array of all file paths in PhysLean.
-/
+@[expose] public section
+
open System
/-- The recursive function underlying `allFilePaths`. -/
diff --git a/PhysLean/Meta/Basic.lean b/PhysLean/Meta/Basic.lean
index 00964ea57..cd3e38640 100644
--- a/PhysLean/Meta/Basic.lean
+++ b/PhysLean/Meta/Basic.lean
@@ -3,14 +3,19 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import Mathlib.Lean.Expr.Basic
-import ImportGraph.Imports.RequiredModules
+module
+
+public import Mathlib.Lean.Expr.Basic
+public import ImportGraph.Imports.RequiredModules
+public import Lean.Elab.DocString
/-!
## Basic Lean meta programming commands
-/
+@[expose] public section
+
/-- The size of a flattened array of arrays. -/
def Array.flatSize {α} : Array (Array α) → Nat :=
foldl (init := 0) fun sizeAcc as => sizeAcc + as.size
@@ -100,15 +105,18 @@ def lineNumber (c : Name) : m Nat := do
/-- Given a name, returns the file name corresponding to that declaration. -/
def fileName (c : Name) : m Name := do
let env ← getEnv
- match env.getModuleFor? c with
- | some decl => return decl
+ match env.getModuleIdxFor? c with
+ | some idx =>
+ pure <| env.header.moduleNames[idx]!
| none => panic! s!"{c} is a declaration without position"
/-- Returns the location of a name. -/
def location (c : Name) : m String := do
let env ← getEnv
- match env.getModuleFor? c with
- | some decl => return s!"{decl.toRelativeFilePath}:{← c.lineNumber} {c}"
+ match env.getModuleIdxFor? c with
+ | some idx =>
+ let modName := env.header.moduleNames[idx]!
+ pure s!"{modName.toRelativeFilePath}:{← c.lineNumber} {c}"
| none => panic! s!"{c} is a declaration without position"
/-- Determines if a name has a location. -/
@@ -119,23 +127,25 @@ def hasPos (c : Name) : m Bool := do
/-- Determines if a name has a doc string. -/
def hasDocString (c : Name) : CoreM Bool := do
let env ← getEnv
- let doc? ← findDocString? env c
- return doc?.isSome
+ return (← findInternalDocString? env c).isSome
/-- The doc string from a name. -/
def getDocString (c : Name) : CoreM String := do
let env ← getEnv
- let doc? ← findDocString? env c
- return doc?.getD ""
+ match ← findInternalDocString? env c with
+ | some (.inl s) => return s
+ | some (.inr _) => return "" -- Verso docstring, ignore for now
+ | none => return ""
/-- Given a name, returns the source code defining that name, including doc strings. -/
def getDeclString (name : Name) : CoreM String := do
let env ← getEnv
match ← findDeclarationRanges? name with
| some { range := { pos, endPos, .. }, .. } =>
- match env.getModuleFor? name with
- | some fileName =>
- let fileContent ← IO.FS.readFile fileName.toRelativeFilePath
+ match env.getModuleIdxFor? name with
+ | some idx =>
+ let modName := env.header.moduleNames[idx]!
+ let fileContent ← IO.FS.readFile modName.toRelativeFilePath
let fileMap := fileContent.toFileMap
return (String.Pos.Raw.extract fileMap.source)
(fileMap.ofPosition pos) (fileMap.ofPosition endPos)
diff --git a/PhysLean/Meta/Informal/Basic.lean b/PhysLean/Meta/Informal/Basic.lean
index e66fef65c..766837f53 100644
--- a/PhysLean/Meta/Informal/Basic.lean
+++ b/PhysLean/Meta/Informal/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import Lean.Parser.Term
+module
+
+public meta import Lean.Parser.Term
/-!
## Informal definitions and lemmas
@@ -15,6 +17,8 @@ Everything else about informal definitions and lemmas are in the `Informal.Post`
-/
+@[expose] public section
+
/-- The structure representing an informal definition. -/
structure InformalDefinition where
/-- The names of top-level commands we expect this definition to depend on. -/
diff --git a/PhysLean/Meta/Informal/Post.lean b/PhysLean/Meta/Informal/Post.lean
index 74aef0269..2aa40c0ef 100644
--- a/PhysLean/Meta/Informal/Post.lean
+++ b/PhysLean/Meta/Informal/Post.lean
@@ -3,14 +3,18 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.Basic
-import PhysLean.Meta.Informal.Basic
-import PhysLean.Meta.TODO.Basic
+module
+
+public import PhysLean.Meta.Basic
+public import PhysLean.Meta.Informal.Basic
+public import PhysLean.Meta.TODO.Basic
/-!
## Informal definitions and lemmas
-/
+
+@[expose] public section
open Lean
namespace Informal
diff --git a/PhysLean/Meta/Informal/SemiFormal.lean b/PhysLean/Meta/Informal/SemiFormal.lean
index 4ec0de1eb..b219c0f8e 100644
--- a/PhysLean/Meta/Informal/SemiFormal.lean
+++ b/PhysLean/Meta/Informal/SemiFormal.lean
@@ -3,7 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import Lean.Elab.Command
+module
+
+public meta import Lean.Elab.Command
+
/-!
# Semiformal results
@@ -19,6 +22,8 @@ David Thrane Christiansen.
-/
+@[expose] public section
+
open Lean Parser Elab Command
/-- The information from a `TODO ...` command. -/
@@ -35,7 +40,7 @@ structure WantedInfo where
tag : String
/-- The environment extension for semiformal results. -/
-initialize wantedExtension : SimplePersistentEnvExtension WantedInfo (Array WantedInfo) ←
+meta initialize wantedExtension : SimplePersistentEnvExtension WantedInfo (Array WantedInfo) ←
registerSimplePersistentEnvExtension {
name := `wantedExtension
addEntryFn := fun arr todoInfor => arr.push todoInfor
@@ -52,12 +57,12 @@ With minor modification they act in a similar way to `proof_wanted`, however
they appear in PhysLean's TODO list and must be tagged accordingly.
They must also always have a doc-string. -/
@[command_parser]
-def «semiformal_result» := leading_parser
+meta def «semiformal_result» := leading_parser
docComment >> "semiformal_result" >> strLit >> declId >> ppIndent declSig
/-- The elaborator for semiformal results. -/
@[command_elab «semiformal_result»]
-def elabLemmaWanted : CommandElab := fun stx =>
+meta def elabLemmaWanted : CommandElab := fun stx =>
match stx with
| `($doc:docComment semiformal_result $s $name $args* : $res) =>
let tag : String := s.getString
diff --git a/PhysLean/Meta/Linters/Sorry.lean b/PhysLean/Meta/Linters/Sorry.lean
index eb360e432..6abd415c8 100644
--- a/PhysLean/Meta/Linters/Sorry.lean
+++ b/PhysLean/Meta/Linters/Sorry.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.Basic
+module
+
+public meta import PhysLean.Meta.Basic
/-!
# The linter for `sorry` declarations and the sorryful attribute
@@ -24,6 +26,8 @@ to be downloaded.
-/
+@[expose] public meta section
+
/-!
## The sorryful environment extension
diff --git a/PhysLean/Meta/Notes/Basic.lean b/PhysLean/Meta/Notes/Basic.lean
index c510bed54..b447e1e16 100644
--- a/PhysLean/Meta/Notes/Basic.lean
+++ b/PhysLean/Meta/Notes/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import Lean.Elab.Command
+module
+
+public meta import Lean.Elab.Command
/-!
## Underlying structure for notes
@@ -20,6 +22,8 @@ Other results relating to notes are in other files.
-/
+@[expose] public section
+
namespace PhysLean
open Lean
@@ -33,7 +37,7 @@ structure NoteInfo where
line : Nat
/-- Environment extension to store `note ...`. -/
-initialize noteExtension : SimplePersistentEnvExtension NoteInfo (Array NoteInfo) ←
+meta initialize noteExtension : SimplePersistentEnvExtension NoteInfo (Array NoteInfo) ←
registerSimplePersistentEnvExtension {
name := `noteExtension
addEntryFn := fun arr nodeInfor => arr.push nodeInfor
@@ -45,7 +49,7 @@ syntax (name := note_comment) "note " str : command
/-- Elaborator for the `note ...` command -/
@[command_elab note_comment]
-def elabNote : Lean.Elab.Command.CommandElab := fun stx =>
+meta def elabNote : Lean.Elab.Command.CommandElab := fun stx =>
match stx with
| `(note $s) => do
let str : String := s.getString
@@ -70,7 +74,7 @@ def elabNote : Lean.Elab.Command.CommandElab := fun stx =>
-/
/-- Environment extension to store `note_attr`. -/
-initialize noteDeclExtension : SimplePersistentEnvExtension Name (Array Name) ←
+meta initialize noteDeclExtension : SimplePersistentEnvExtension Name (Array Name) ←
registerSimplePersistentEnvExtension {
name := `noteDeclExtension
addEntryFn := fun arr nodeInfor => arr.push nodeInfor
@@ -78,7 +82,7 @@ initialize noteDeclExtension : SimplePersistentEnvExtension Name (Array Name)
}
/-- The `note_attr` attribute is used to display formally verified commands within a note. -/
-initialize noteAttribute : Unit ←
+meta initialize noteAttribute : Unit ←
registerBuiltinAttribute {
name := `note_attr
descr := "Note attribute"
@@ -88,7 +92,7 @@ initialize noteAttribute : Unit ←
}
/-- Environment extension to store `note_attr_informal`. -/
-initialize noteInformalDeclExtension : SimplePersistentEnvExtension Name (Array Name) ←
+meta initialize noteInformalDeclExtension : SimplePersistentEnvExtension Name (Array Name) ←
registerSimplePersistentEnvExtension {
name := `noteInformalDeclExtension
addEntryFn := fun arr nodeInfor => arr.push nodeInfor
@@ -96,7 +100,7 @@ initialize noteInformalDeclExtension : SimplePersistentEnvExtension Name (Array
}
/-- The `note_attr_informal` attribute is used to display informal commands within a note. -/
-initialize noteInformalAttribute : Unit ←
+meta initialize noteInformalAttribute : Unit ←
registerBuiltinAttribute {
name := `note_attr_informal
descr := "Informal note attribute"
diff --git a/PhysLean/Meta/Notes/HTMLNote.lean b/PhysLean/Meta/Notes/HTMLNote.lean
index bab1782fb..a1b4d5ee1 100644
--- a/PhysLean/Meta/Notes/HTMLNote.lean
+++ b/PhysLean/Meta/Notes/HTMLNote.lean
@@ -4,15 +4,19 @@ Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-- import DocGen4.Output.DocString
-import PhysLean.Meta.Basic
-import PhysLean.Meta.Notes.Basic
-import PhysLean.Meta.Informal.Basic
+module
+
+public import PhysLean.Meta.Basic
+public import PhysLean.Meta.Notes.Basic
+public import PhysLean.Meta.Informal.Basic
/-!
## Turns a declaration into a html note structure.
-/
+@[expose] public section
+
namespace PhysLean
open Lean
diff --git a/PhysLean/Meta/Notes/NoteFile.lean b/PhysLean/Meta/Notes/NoteFile.lean
index 29379f316..4a5523c5a 100644
--- a/PhysLean/Meta/Notes/NoteFile.lean
+++ b/PhysLean/Meta/Notes/NoteFile.lean
@@ -3,7 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import Lean.Environment
+module
+
+public import Lean.Environment
/-!
# Note file
@@ -12,6 +14,8 @@ A note file is a structure which contains the information to go into a note.
-/
+@[expose] public section
+
namespace PhysLean
open Lean
diff --git a/PhysLean/Meta/Notes/ToHTML.lean b/PhysLean/Meta/Notes/ToHTML.lean
index 6fc64db62..9e6ce35e2 100644
--- a/PhysLean/Meta/Notes/ToHTML.lean
+++ b/PhysLean/Meta/Notes/ToHTML.lean
@@ -3,14 +3,18 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
-import PhysLean.Meta.Notes.HTMLNote
-import PhysLean.Meta.Notes.NoteFile
+module
+
+public meta import PhysLean.Meta.Notes.HTMLNote
+public import PhysLean.Meta.Notes.NoteFile
/-!
## Turns a declaration into a html note structure.
-/
+@[expose] public section
+
namespace PhysLean
open Lean System Meta
@@ -18,14 +22,14 @@ namespace NoteFile
variable (N : NoteFile)
/-- Sorts `NoteInfo`'s by file name then by line number. -/
-def sortLE (ni1 ni2 : HTMLNote) : Bool :=
+meta def sortLE (ni1 ni2 : HTMLNote) : Bool :=
if N.files.idxOf ni1.fileName ≠ N.files.idxOf ni2.fileName
then N.files.idxOf ni1.fileName ≤ N.files.idxOf ni2.fileName
else
ni1.line ≤ ni2.line
/-- Returns a sorted list of NodeInfos for a file system. -/
-unsafe def getNodeInfo : CoreM (List HTMLNote) := do
+meta unsafe def getNodeInfo : CoreM (List HTMLNote) := do
let env ← getEnv
let allNotes := (noteExtension.getState env)
let allDecl := (noteDeclExtension.getState env)
@@ -37,7 +41,7 @@ unsafe def getNodeInfo : CoreM (List HTMLNote) := do
pure noteInfoSort
/-- The HTML code needed to have syntax highlighting. -/
-def codeBlockHTML : String := "
+meta def codeBlockHTML : String := "
@@ -65,7 +69,7 @@ def codeBlockHTML : String := "
"
/-- The html styles for informal definitions. -/
-def informalDefStyle : String :=
+meta def informalDefStyle : String :=
"