From 905011b23435b5b955334992325709cd9e829c88 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:27:11 +0100 Subject: [PATCH 1/7] refactor: The move --- Physlib.lean | 50 +++++++++---------- .../SimplePendulum/PeriodFormula.lean | 2 +- .../RigidBody/AngularMomentum.lean | 2 +- .../RigidBody/AngularVelocity.lean | 7 +-- .../RigidBody/KineticEnergy.lean | 2 +- Physlib/Mathematics/Calculus/AdjFDeriv.lean | 2 +- .../DataStructures/FourTree/Basic.lean | 0 .../DataStructures/FourTree/UniqueMap.lean | 2 +- .../DataStructures/Matrix/LieTrace.lean | 2 +- .../{ => ForMathlib}/FDerivCurry.lean | 0 Physlib/Mathematics/{ => ForMathlib}/Fin.lean | 0 .../{ => ForMathlib}/Fin/Involutions.lean | 0 .../Metric/PseudoRiemannian/Defs.lean | 0 .../Geometry/Metric/Riemannian/Defs.lean | 2 +- .../{ => ForMathlib}/HasTemperateGrowth.lean | 0 .../{ => ForMathlib}/LinearMaps.lean | 0 .../{ => ForMathlib}/LinearPMap.lean | 0 .../Mathematics/{ => ForMathlib}/List.lean | 2 +- .../{ => ForMathlib}/List/InsertIdx.lean | 0 .../{ => ForMathlib}/List/InsertionSort.lean | 4 +- .../OneParameterSubgroups/Basic.lean | 2 +- .../OneParameterSubgroups/Unitary.lean | 2 +- .../{ => ForMathlib}/OrthogonalMatrix.lean | 0 .../{ => ForMathlib}/PiTensorProduct.lean | 0 .../{ => ForMathlib}/Resolvent.lean | 0 .../{ => ForMathlib}/SchurTriangulation.lean | 0 .../{ => ForMathlib}/Trigonometry/SinSq.lean | 0 .../{ => ForMathlib}/Trigonometry/Tanh.lean | 0 .../Mathematics/{ => Modules}/ConjModule.lean | 0 .../{ => Modules}/CrossProduct.lean | 0 .../{ => Modules}/CrossProductMatrix.lean | 0 Physlib/Meta/Linters/DefsWithUnderscore.lean | 3 +- Physlib/QFT/AnomalyCancellation/Basic.lean | 2 +- .../FieldSpecification/CrAnSection.lean | 2 +- .../FieldStatistics/Basic.lean | 2 +- .../PerturbationTheory/Koszul/KoszulSign.lean | 4 +- .../Koszul/KoszulSignInsert.lean | 2 +- .../WickContraction/Erase.lean | 2 +- .../WickContraction/IsFull.lean | 2 +- Physlib/QuantumMechanics/FiniteTarget.lean | 2 +- .../HarmonicOscillator/Eigenstates.lean | 2 +- .../QuantumMechanics/Operators/API-map.yaml | 2 +- .../Operators/SpectralTheory/API-map.yaml | 2 +- .../QuantumMechanics/Operators/Unbounded.lean | 2 +- .../QuantumMechanics/PoschlTeller/Basic.lean | 2 +- .../LorentzAlgebra/ExponentialMap.lean | 2 +- Physlib/Relativity/SL2C/Basic.lean | 2 +- .../Relativity/Tensors/Conjugation/Basic.lean | 11 ++-- .../HilbertSpace/Dynamics/Automorphism.lean | 2 +- scripts/MetaPrograms/module_doc_no_lint.txt | 38 +++++++------- 50 files changed, 85 insertions(+), 82 deletions(-) rename Physlib/Mathematics/{ => ForMathlib}/DataStructures/FourTree/Basic.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/DataStructures/FourTree/UniqueMap.lean (99%) rename Physlib/Mathematics/{ => ForMathlib}/DataStructures/Matrix/LieTrace.lean (99%) rename Physlib/Mathematics/{ => ForMathlib}/FDerivCurry.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Fin.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Fin/Involutions.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Geometry/Metric/PseudoRiemannian/Defs.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Geometry/Metric/Riemannian/Defs.lean (99%) rename Physlib/Mathematics/{ => ForMathlib}/HasTemperateGrowth.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/LinearMaps.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/LinearPMap.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/List.lean (99%) rename Physlib/Mathematics/{ => ForMathlib}/List/InsertIdx.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/List/InsertionSort.lean (99%) rename Physlib/Mathematics/{ => ForMathlib}/OneParameterSubgroups/Basic.lean (98%) rename Physlib/Mathematics/{ => ForMathlib}/OneParameterSubgroups/Unitary.lean (99%) rename Physlib/Mathematics/{ => ForMathlib}/OrthogonalMatrix.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/PiTensorProduct.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Resolvent.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/SchurTriangulation.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Trigonometry/SinSq.lean (100%) rename Physlib/Mathematics/{ => ForMathlib}/Trigonometry/Tanh.lean (100%) rename Physlib/Mathematics/{ => Modules}/ConjModule.lean (100%) rename Physlib/Mathematics/{ => Modules}/CrossProduct.lean (100%) rename Physlib/Mathematics/{ => Modules}/CrossProductMatrix.lean (100%) diff --git a/Physlib.lean b/Physlib.lean index 3a15298bf2..d3511ffa09 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -119,20 +119,30 @@ public import Physlib.Mathematics.Calculus.Gradient public import Physlib.Mathematics.Calculus.ParametricIntegration public import Physlib.Mathematics.Calculus.Wirtinger.Basic public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate -public import Physlib.Mathematics.ConjModule -public import Physlib.Mathematics.CrossProduct -public import Physlib.Mathematics.CrossProductMatrix -public import Physlib.Mathematics.DataStructures.FourTree.Basic -public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap -public import Physlib.Mathematics.DataStructures.Matrix.LieTrace public import Physlib.Mathematics.Distribution.Basic public import Physlib.Mathematics.Distribution.PowMul -public import Physlib.Mathematics.FDerivCurry -public import Physlib.Mathematics.Fin -public import Physlib.Mathematics.Fin.Involutions -public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs -public import Physlib.Mathematics.Geometry.Metric.Riemannian.Defs -public import Physlib.Mathematics.HasTemperateGrowth +public import Physlib.Mathematics.ForMathlib.DataStructures.FourTree.Basic +public import Physlib.Mathematics.ForMathlib.DataStructures.FourTree.UniqueMap +public import Physlib.Mathematics.ForMathlib.DataStructures.Matrix.LieTrace +public import Physlib.Mathematics.ForMathlib.FDerivCurry +public import Physlib.Mathematics.ForMathlib.Fin +public import Physlib.Mathematics.ForMathlib.Fin.Involutions +public import Physlib.Mathematics.ForMathlib.Geometry.Metric.PseudoRiemannian.Defs +public import Physlib.Mathematics.ForMathlib.Geometry.Metric.Riemannian.Defs +public import Physlib.Mathematics.ForMathlib.HasTemperateGrowth +public import Physlib.Mathematics.ForMathlib.LinearMaps +public import Physlib.Mathematics.ForMathlib.LinearPMap +public import Physlib.Mathematics.ForMathlib.List +public import Physlib.Mathematics.ForMathlib.List.InsertIdx +public import Physlib.Mathematics.ForMathlib.List.InsertionSort +public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Basic +public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Unitary +public import Physlib.Mathematics.ForMathlib.OrthogonalMatrix +public import Physlib.Mathematics.ForMathlib.PiTensorProduct +public import Physlib.Mathematics.ForMathlib.Resolvent +public import Physlib.Mathematics.ForMathlib.SchurTriangulation +public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq +public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh public import Physlib.Mathematics.InnerProductSpace.Adjoint public import Physlib.Mathematics.InnerProductSpace.Basic public import Physlib.Mathematics.InnerProductSpace.Calculus @@ -141,22 +151,12 @@ public import Physlib.Mathematics.InnerProductSpace.Submodule public import Physlib.Mathematics.KroneckerDelta.Basic public import Physlib.Mathematics.KroneckerDelta.Contraction public import Physlib.Mathematics.LeviCivita.Basic -public import Physlib.Mathematics.LinearMaps -public import Physlib.Mathematics.LinearPMap -public import Physlib.Mathematics.List -public import Physlib.Mathematics.List.InsertIdx -public import Physlib.Mathematics.List.InsertionSort -public import Physlib.Mathematics.OneParameterSubgroups.Basic -public import Physlib.Mathematics.OneParameterSubgroups.Unitary -public import Physlib.Mathematics.OrthogonalMatrix -public import Physlib.Mathematics.PiTensorProduct -public import Physlib.Mathematics.Resolvent +public import Physlib.Mathematics.Modules.ConjModule +public import Physlib.Mathematics.Modules.CrossProduct +public import Physlib.Mathematics.Modules.CrossProductMatrix public import Physlib.Mathematics.SO3.Basic -public import Physlib.Mathematics.SchurTriangulation public import Physlib.Mathematics.SpecialFunctions.EllipticIntegral public import Physlib.Mathematics.SpecialFunctions.PhysHermite -public import Physlib.Mathematics.Trigonometry.SinSq -public import Physlib.Mathematics.Trigonometry.Tanh public import Physlib.Mathematics.VariationalCalculus.Basic public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv public import Physlib.Mathematics.VariationalCalculus.HasVarAdjoint diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean index 31be1054c2..cc08d922d6 100644 --- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean +++ b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean @@ -7,7 +7,7 @@ module public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.SmallAngle public import Physlib.Mathematics.SpecialFunctions.EllipticIntegral -public import Physlib.Mathematics.Trigonometry.SinSq +public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq /-! # The period formula of the simple gravity pendulum diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean b/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean index 063a3b0380..fda006b223 100644 --- a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean +++ b/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean @@ -6,7 +6,7 @@ Authors: Giuseppe Sorge module public import Physlib.ClassicalMechanics.RigidBody.Basic -public import Physlib.Mathematics.CrossProduct +public import Physlib.Mathematics.Modules.CrossProduct /-! # Angular momentum of a rigid body diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean b/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean index d8f8dc8a62..041dab711f 100644 --- a/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean +++ b/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean @@ -6,7 +6,7 @@ Authors: Giuseppe Sorge module public import Physlib.ClassicalMechanics.RigidBody.Motion -public import Physlib.Mathematics.CrossProductMatrix +public import Physlib.Mathematics.Modules.CrossProductMatrix /-! # The angular velocity of a rigid body @@ -22,8 +22,9 @@ rules for time derivatives of matrices used for this live in `Physlib.SpaceAndTime.Time.MatrixDerivatives`. In three dimensions the skew-symmetric tensor `Ω` is dual to the *angular velocity vector* -`ω(t) = Ωᵛ` via the hat map (`Physlib.Mathematics.CrossProductMatrix`), with `[ω]ₓ = Ω`; `ω` is the -angular velocity proper, appearing in the decomposition `v = V + ω × r` as an honest cross product. +`ω(t) = Ωᵛ` via the hat map (`Physlib.Mathematics.Modules.CrossProductMatrix`), with +`[ω]ₓ = Ω`; `ω` is the angular velocity proper, appearing in the decomposition `v = V + ω × r` +as an honest cross product. The angular velocity can equally be expressed in the *body frame*: the moving coordinate system rigidly attached to the body, with origin at the centre of mass and axes rotating with the body, diff --git a/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean b/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean index f7731c7bb2..85a7b079c3 100644 --- a/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean +++ b/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean @@ -7,7 +7,7 @@ module public import Physlib.ClassicalMechanics.RigidBody.AngularMomentum public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity -public import Physlib.Mathematics.OrthogonalMatrix +public import Physlib.Mathematics.ForMathlib.OrthogonalMatrix /-! # Kinetic energy of a rigid body diff --git a/Physlib/Mathematics/Calculus/AdjFDeriv.lean b/Physlib/Mathematics/Calculus/AdjFDeriv.lean index 16130eb113..78d97ef40f 100644 --- a/Physlib/Mathematics/Calculus/AdjFDeriv.lean +++ b/Physlib/Mathematics/Calculus/AdjFDeriv.lean @@ -6,7 +6,7 @@ Authors: Tomas Skrivan module public import Mathlib.Analysis.Calculus.Gradient.Basic -public import Physlib.Mathematics.FDerivCurry +public import Physlib.Mathematics.ForMathlib.FDerivCurry public import Physlib.Mathematics.InnerProductSpace.Adjoint public import Physlib.Mathematics.InnerProductSpace.Calculus /-! diff --git a/Physlib/Mathematics/DataStructures/FourTree/Basic.lean b/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean similarity index 100% rename from Physlib/Mathematics/DataStructures/FourTree/Basic.lean rename to Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean diff --git a/Physlib/Mathematics/DataStructures/FourTree/UniqueMap.lean b/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean similarity index 99% rename from Physlib/Mathematics/DataStructures/FourTree/UniqueMap.lean rename to Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean index c1064d0f3a..a92042f67f 100644 --- a/Physlib/Mathematics/DataStructures/FourTree/UniqueMap.lean +++ b/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.DataStructures.FourTree.Basic +public import Physlib.Mathematics.ForMathlib.DataStructures.FourTree.Basic /-! ## Unique maps for `FourTree` diff --git a/Physlib/Mathematics/DataStructures/Matrix/LieTrace.lean b/Physlib/Mathematics/ForMathlib/DataStructures/Matrix/LieTrace.lean similarity index 99% rename from Physlib/Mathematics/DataStructures/Matrix/LieTrace.lean rename to Physlib/Mathematics/ForMathlib/DataStructures/Matrix/LieTrace.lean index c2b36501ba..0c425136ef 100644 --- a/Physlib/Mathematics/DataStructures/Matrix/LieTrace.lean +++ b/Physlib/Mathematics/ForMathlib/DataStructures/Matrix/LieTrace.lean @@ -7,7 +7,7 @@ module public import Mathlib.Analysis.Complex.Polynomial.Basic public import Mathlib.Analysis.Normed.Algebra.MatrixExponential -public import Physlib.Mathematics.SchurTriangulation +public import Physlib.Mathematics.ForMathlib.SchurTriangulation /-! # Lie's Trace Formula diff --git a/Physlib/Mathematics/FDerivCurry.lean b/Physlib/Mathematics/ForMathlib/FDerivCurry.lean similarity index 100% rename from Physlib/Mathematics/FDerivCurry.lean rename to Physlib/Mathematics/ForMathlib/FDerivCurry.lean diff --git a/Physlib/Mathematics/Fin.lean b/Physlib/Mathematics/ForMathlib/Fin.lean similarity index 100% rename from Physlib/Mathematics/Fin.lean rename to Physlib/Mathematics/ForMathlib/Fin.lean diff --git a/Physlib/Mathematics/Fin/Involutions.lean b/Physlib/Mathematics/ForMathlib/Fin/Involutions.lean similarity index 100% rename from Physlib/Mathematics/Fin/Involutions.lean rename to Physlib/Mathematics/ForMathlib/Fin/Involutions.lean diff --git a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean similarity index 100% rename from Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean rename to Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean diff --git a/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean b/Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean similarity index 99% rename from Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean rename to Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean index a588dc5b3e..17f7da09fe 100644 --- a/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean +++ b/Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean @@ -5,7 +5,7 @@ Authors: Matteo Cipollina -/ module -public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs +public import Physlib.Mathematics.ForMathlib.Geometry.Metric.PseudoRiemannian.Defs public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic /-! # Riemannian Metric Definitions diff --git a/Physlib/Mathematics/HasTemperateGrowth.lean b/Physlib/Mathematics/ForMathlib/HasTemperateGrowth.lean similarity index 100% rename from Physlib/Mathematics/HasTemperateGrowth.lean rename to Physlib/Mathematics/ForMathlib/HasTemperateGrowth.lean diff --git a/Physlib/Mathematics/LinearMaps.lean b/Physlib/Mathematics/ForMathlib/LinearMaps.lean similarity index 100% rename from Physlib/Mathematics/LinearMaps.lean rename to Physlib/Mathematics/ForMathlib/LinearMaps.lean diff --git a/Physlib/Mathematics/LinearPMap.lean b/Physlib/Mathematics/ForMathlib/LinearPMap.lean similarity index 100% rename from Physlib/Mathematics/LinearPMap.lean rename to Physlib/Mathematics/ForMathlib/LinearPMap.lean diff --git a/Physlib/Mathematics/List.lean b/Physlib/Mathematics/ForMathlib/List.lean similarity index 99% rename from Physlib/Mathematics/List.lean rename to Physlib/Mathematics/ForMathlib/List.lean index 717c410560..68a8f7af34 100644 --- a/Physlib/Mathematics/List.lean +++ b/Physlib/Mathematics/ForMathlib/List.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.Fin +public import Physlib.Mathematics.ForMathlib.Fin public import Mathlib.Order.Lattice.Nat public import Mathlib.Data.List.TakeWhile import all Mathlib.Data.List.Sort diff --git a/Physlib/Mathematics/List/InsertIdx.lean b/Physlib/Mathematics/ForMathlib/List/InsertIdx.lean similarity index 100% rename from Physlib/Mathematics/List/InsertIdx.lean rename to Physlib/Mathematics/ForMathlib/List/InsertIdx.lean diff --git a/Physlib/Mathematics/List/InsertionSort.lean b/Physlib/Mathematics/ForMathlib/List/InsertionSort.lean similarity index 99% rename from Physlib/Mathematics/List/InsertionSort.lean rename to Physlib/Mathematics/ForMathlib/List/InsertionSort.lean index aa91457725..2accf1ba85 100644 --- a/Physlib/Mathematics/List/InsertionSort.lean +++ b/Physlib/Mathematics/ForMathlib/List/InsertionSort.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.List -import all Physlib.Mathematics.List +public import Physlib.Mathematics.ForMathlib.List +import all Physlib.Mathematics.ForMathlib.List /-! # List lemmas diff --git a/Physlib/Mathematics/OneParameterSubgroups/Basic.lean b/Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Basic.lean similarity index 98% rename from Physlib/Mathematics/OneParameterSubgroups/Basic.lean rename to Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Basic.lean index 3b9ae59a6c..e0f7e591a0 100644 --- a/Physlib/Mathematics/OneParameterSubgroups/Basic.lean +++ b/Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Basic.lean @@ -21,7 +21,7 @@ Let `E` be a real Banach algebra. This file proves that every continuous additiv This is the Banach-algebra argument underlying the correspondence between norm-continuous unitary one-parameter groups and bounded self-adjoint generators. See -`Physlib.Mathematics.OneParameterSubgroups.Unitary` for that correspondence. +`Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Unitary` for that correspondence. **Proof outline.** Continuity at zero implies that, for sufficiently small `d > 0`, the integral of `U` over `[0, d]` is close to `d • 1` and therefore invertible. If `I` is the indefinite integral of diff --git a/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean b/Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Unitary.lean similarity index 99% rename from Physlib/Mathematics/OneParameterSubgroups/Unitary.lean rename to Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Unitary.lean index 110fc3e180..0817b36418 100644 --- a/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean +++ b/Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Unitary.lean @@ -7,7 +7,7 @@ module public import Mathlib.Analysis.InnerProductSpace.Adjoint public import Mathlib.Analysis.Calculus.Deriv.Star -public import Physlib.Mathematics.OneParameterSubgroups.Basic +public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Basic /-! diff --git a/Physlib/Mathematics/OrthogonalMatrix.lean b/Physlib/Mathematics/ForMathlib/OrthogonalMatrix.lean similarity index 100% rename from Physlib/Mathematics/OrthogonalMatrix.lean rename to Physlib/Mathematics/ForMathlib/OrthogonalMatrix.lean diff --git a/Physlib/Mathematics/PiTensorProduct.lean b/Physlib/Mathematics/ForMathlib/PiTensorProduct.lean similarity index 100% rename from Physlib/Mathematics/PiTensorProduct.lean rename to Physlib/Mathematics/ForMathlib/PiTensorProduct.lean diff --git a/Physlib/Mathematics/Resolvent.lean b/Physlib/Mathematics/ForMathlib/Resolvent.lean similarity index 100% rename from Physlib/Mathematics/Resolvent.lean rename to Physlib/Mathematics/ForMathlib/Resolvent.lean diff --git a/Physlib/Mathematics/SchurTriangulation.lean b/Physlib/Mathematics/ForMathlib/SchurTriangulation.lean similarity index 100% rename from Physlib/Mathematics/SchurTriangulation.lean rename to Physlib/Mathematics/ForMathlib/SchurTriangulation.lean diff --git a/Physlib/Mathematics/Trigonometry/SinSq.lean b/Physlib/Mathematics/ForMathlib/Trigonometry/SinSq.lean similarity index 100% rename from Physlib/Mathematics/Trigonometry/SinSq.lean rename to Physlib/Mathematics/ForMathlib/Trigonometry/SinSq.lean diff --git a/Physlib/Mathematics/Trigonometry/Tanh.lean b/Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean similarity index 100% rename from Physlib/Mathematics/Trigonometry/Tanh.lean rename to Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean diff --git a/Physlib/Mathematics/ConjModule.lean b/Physlib/Mathematics/Modules/ConjModule.lean similarity index 100% rename from Physlib/Mathematics/ConjModule.lean rename to Physlib/Mathematics/Modules/ConjModule.lean diff --git a/Physlib/Mathematics/CrossProduct.lean b/Physlib/Mathematics/Modules/CrossProduct.lean similarity index 100% rename from Physlib/Mathematics/CrossProduct.lean rename to Physlib/Mathematics/Modules/CrossProduct.lean diff --git a/Physlib/Mathematics/CrossProductMatrix.lean b/Physlib/Mathematics/Modules/CrossProductMatrix.lean similarity index 100% rename from Physlib/Mathematics/CrossProductMatrix.lean rename to Physlib/Mathematics/Modules/CrossProductMatrix.lean diff --git a/Physlib/Meta/Linters/DefsWithUnderscore.lean b/Physlib/Meta/Linters/DefsWithUnderscore.lean index 8202d9bfab..228d233b68 100644 --- a/Physlib/Meta/Linters/DefsWithUnderscore.lean +++ b/Physlib/Meta/Linters/DefsWithUnderscore.lean @@ -25,7 +25,8 @@ either generated by Lean or belongs to a declaration that is not user-facing: across projects, `_physlib` for a declaration in `Physlib` and so on. Mathlib exempts its own `_mathlib` suffix in the same way. * Anonymous instances that Lean disambiguates with a trailing number. Mathlib exempts `_1` and - `_2` but not `_3` and `_4`, which occur in `Physlib.Mathematics.DataStructures.FourTree.Basic`. + `_2` but not `_3` and `_4`, which occur in + `Physlib.Mathematics.ForMathlib.DataStructures.FourTree.Basic`. `withDefsWithUnderscoreExemptions` wraps the linter so that these pass; every other declaration is reported as before. diff --git a/Physlib/QFT/AnomalyCancellation/Basic.lean b/Physlib/QFT/AnomalyCancellation/Basic.lean index 4653d24369..6a5e03ac0d 100644 --- a/Physlib/QFT/AnomalyCancellation/Basic.lean +++ b/Physlib/QFT/AnomalyCancellation/Basic.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.LinearMaps +public import Physlib.Mathematics.ForMathlib.LinearMaps public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.Tactic.Cases /-! diff --git a/Physlib/QFT/PerturbationTheory/FieldSpecification/CrAnSection.lean b/Physlib/QFT/PerturbationTheory/FieldSpecification/CrAnSection.lean index 6f458c7485..f86278b238 100644 --- a/Physlib/QFT/PerturbationTheory/FieldSpecification/CrAnSection.lean +++ b/Physlib/QFT/PerturbationTheory/FieldSpecification/CrAnSection.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp -public import Physlib.Mathematics.List +public import Physlib.Mathematics.ForMathlib.List /-! # Creation and annihilation sections diff --git a/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean b/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean index 46fd97a584..f2932e8588 100644 --- a/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean +++ b/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.List.InsertIdx +public import Physlib.Mathematics.ForMathlib.List.InsertIdx public import Mathlib.Tactic.FinCases public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise public import Mathlib.Data.Fintype.Card diff --git a/Physlib/QFT/PerturbationTheory/Koszul/KoszulSign.lean b/Physlib/QFT/PerturbationTheory/Koszul/KoszulSign.lean index da5ccf2cb8..90afca0944 100644 --- a/Physlib/QFT/PerturbationTheory/Koszul/KoszulSign.lean +++ b/Physlib/QFT/PerturbationTheory/Koszul/KoszulSign.lean @@ -5,8 +5,8 @@ Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.Koszul.KoszulSignInsert -public import Physlib.Mathematics.List.InsertionSort -import all Physlib.Mathematics.List +public import Physlib.Mathematics.ForMathlib.List.InsertionSort +import all Physlib.Mathematics.ForMathlib.List /-! # Koszul sign diff --git a/Physlib/QFT/PerturbationTheory/Koszul/KoszulSignInsert.lean b/Physlib/QFT/PerturbationTheory/Koszul/KoszulSignInsert.lean index 871de85e52..f58fd6b277 100644 --- a/Physlib/QFT/PerturbationTheory/Koszul/KoszulSignInsert.lean +++ b/Physlib/QFT/PerturbationTheory/Koszul/KoszulSignInsert.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.FieldStatistics.ExchangeSign -public import Physlib.Mathematics.List +public import Physlib.Mathematics.ForMathlib.List import all Mathlib.Data.List.Sort /-! diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/Erase.lean b/Physlib/QFT/PerturbationTheory/WickContraction/Erase.lean index f531191414..8f8a408b70 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/Erase.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/Erase.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.QFT.PerturbationTheory.WickContraction.Uncontracted -public import Physlib.Mathematics.Fin +public import Physlib.Mathematics.ForMathlib.Fin /-! # Erasing an element from a contraction diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/IsFull.lean b/Physlib/QFT/PerturbationTheory/WickContraction/IsFull.lean index 0e76f2f026..a3a34dd4b0 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/IsFull.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/IsFull.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.Fin.Involutions +public import Physlib.Mathematics.ForMathlib.Fin.Involutions public import Physlib.QFT.PerturbationTheory.WickContraction.ExtractEquiv public import Physlib.QFT.PerturbationTheory.WickContraction.Involutions /-! diff --git a/Physlib/QuantumMechanics/FiniteTarget.lean b/Physlib/QuantumMechanics/FiniteTarget.lean index 86c87d5273..e7360c7815 100644 --- a/Physlib/QuantumMechanics/FiniteTarget.lean +++ b/Physlib/QuantumMechanics/FiniteTarget.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Mathematics.OneParameterSubgroups.Unitary +public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Unitary public import Physlib.Meta.TODO.Basic public import Physlib.QuantumMechanics.PlanckConstant /-! diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean index eabb5d2580..05a8300e4f 100644 --- a/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean +++ b/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean @@ -6,7 +6,7 @@ Authors: Philippe Kevorkian, Gregory J. Loges module public import Physlib.Mathematics.InnerProductSpace.Gaussian -public import Physlib.Mathematics.HasTemperateGrowth +public import Physlib.Mathematics.ForMathlib.HasTemperateGrowth public import Physlib.QuantumMechanics.HarmonicOscillator.NumberOperator public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction public import Physlib.Meta.Linters.Sorry diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml index 0704f8563c..18fc87d8da 100644 --- a/Physlib/QuantumMechanics/Operators/API-map.yaml +++ b/Physlib/QuantumMechanics/Operators/API-map.yaml @@ -39,7 +39,7 @@ ParentAPIs: - "Hilbert spaces on Space (Physlib/QuantumMechanics/HilbertSpaces/SpaceD)" - "Space (Physlib/SpaceAndTime/Space)" - "Planck constant (Physlib/QuantumMechanics/PlanckConstant.lean)" - - "Partially defined linear maps (Physlib/Mathematics/LinearPMap.lean)" + - "Partially defined linear maps (Physlib/Mathematics/ForMathlib/LinearPMap.lean)" - "Inner product spaces (Physlib/Mathematics/InnerProductSpace)" References: diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/API-map.yaml b/Physlib/QuantumMechanics/Operators/SpectralTheory/API-map.yaml index 15a16f8fde..6a9ee6189e 100644 --- a/Physlib/QuantumMechanics/Operators/SpectralTheory/API-map.yaml +++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/API-map.yaml @@ -26,7 +26,7 @@ Overview: | ParentAPIs: - "Operator algebra (Physlib/QuantumMechanics/Operators)" - - "Partially defined linear maps (Physlib/Mathematics/LinearPMap.lean)" + - "Partially defined linear maps (Physlib/Mathematics/ForMathlib/LinearPMap.lean)" - "Inner product spaces (Physlib/Mathematics/InnerProductSpace)" References: diff --git a/Physlib/QuantumMechanics/Operators/Unbounded.lean b/Physlib/QuantumMechanics/Operators/Unbounded.lean index 82cabec42b..a70da00aae 100644 --- a/Physlib/QuantumMechanics/Operators/Unbounded.lean +++ b/Physlib/QuantumMechanics/Operators/Unbounded.lean @@ -6,7 +6,7 @@ Authors: Adam Bornemann, Gregory J. Loges module public import Physlib.Mathematics.InnerProductSpace.Submodule -public import Physlib.Mathematics.LinearPMap +public import Physlib.Mathematics.ForMathlib.LinearPMap public import Physlib.Meta.TODO.Basic /-! diff --git a/Physlib/QuantumMechanics/PoschlTeller/Basic.lean b/Physlib/QuantumMechanics/PoschlTeller/Basic.lean index 329894b003..32d9be5cba 100644 --- a/Physlib/QuantumMechanics/PoschlTeller/Basic.lean +++ b/Physlib/QuantumMechanics/PoschlTeller/Basic.lean @@ -6,7 +6,7 @@ Authors: Afiq Hatta module public import Physlib.QuantumMechanics.SpaceDQuantumSystem -public import Physlib.Mathematics.Trigonometry.Tanh +public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh /-! # 1d Pöschl-Teller diff --git a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean index 3b2b8b6399..f9abbdc3dc 100644 --- a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean +++ b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean @@ -5,7 +5,7 @@ Authors: Matteo Cipollina -/ module -public import Physlib.Mathematics.DataStructures.Matrix.LieTrace +public import Physlib.Mathematics.ForMathlib.DataStructures.Matrix.LieTrace public import Physlib.Relativity.LorentzAlgebra.Basic public import Physlib.Relativity.LorentzGroup.Restricted.Basic diff --git a/Physlib/Relativity/SL2C/Basic.lean b/Physlib/Relativity/SL2C/Basic.lean index 106d604f39..b86e96d460 100644 --- a/Physlib/Relativity/SL2C/Basic.lean +++ b/Physlib/Relativity/SL2C/Basic.lean @@ -8,7 +8,7 @@ module public import Physlib.Relativity.SL2C.SelfAdjoint public import Mathlib.Analysis.Complex.Polynomial.Basic public import Physlib.Relativity.LorentzGroup.Restricted.Basic -public import Physlib.Mathematics.SchurTriangulation +public import Physlib.Mathematics.ForMathlib.SchurTriangulation /-! # The group SL(2, ℂ) and it's relation to the Lorentz group diff --git a/Physlib/Relativity/Tensors/Conjugation/Basic.lean b/Physlib/Relativity/Tensors/Conjugation/Basic.lean index f63d7cbdd9..9319716369 100644 --- a/Physlib/Relativity/Tensors/Conjugation/Basic.lean +++ b/Physlib/Relativity/Tensors/Conjugation/Basic.lean @@ -6,7 +6,7 @@ Authors: Andrea Pari module public import Physlib.Relativity.Tensors.Contraction.Basis -public import Physlib.Mathematics.ConjModule +public import Physlib.Mathematics.Modules.ConjModule /-! @@ -35,10 +35,11 @@ last makes reality and Hermiticity compatible with raising and lowering indices. At the single-index level, `conjEquiv : V c ≃ₛₗ V (bar c)` realises this conjugation: it reads a vector's coordinates, conjugates them with `ConjModule.starFinsupp`, and re-seats them at the -conjugate colour. It rests on the conjugate module `ConjModule` (`Physlib.Mathematics.ConjModule`), -the same vectors with the scalar action twisted by conjugation (`i` acts as `−i`). Equipping the -conjugate colours with such conjugate-module carriers is what makes a metric `V c ⊗ V (bar c) → k` -genuinely bilinear and `IsHermitian` an honest conjugate-transpose. +conjugate colour. It rests on the conjugate module `ConjModule` +(`Physlib.Mathematics.Modules.ConjModule`), the same vectors with the scalar action twisted by +conjugation (`i` acts as `−i`). Equipping the conjugate colours with such conjugate-module +carriers is what makes a metric `V c ⊗ V (bar c) → k` genuinely bilinear and `IsHermitian` an +honest conjugate-transpose. ## ii. Key results diff --git a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Dynamics/Automorphism.lean b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Dynamics/Automorphism.lean index ea3d028bd9..535d7ace8a 100644 --- a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Dynamics/Automorphism.lean +++ b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Dynamics/Automorphism.lean @@ -6,7 +6,7 @@ Authors: Tom Ole Diem module public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Automorphism -public import Physlib.Mathematics.OneParameterSubgroups.Unitary +public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Unitary public import Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv public import Mathlib.Analysis.CStarAlgebra.Hom public import Mathlib.Analysis.InnerProductSpace.StarOrder diff --git a/scripts/MetaPrograms/module_doc_no_lint.txt b/scripts/MetaPrograms/module_doc_no_lint.txt index c222aaf4c7..4ed3350336 100644 --- a/scripts/MetaPrograms/module_doc_no_lint.txt +++ b/scripts/MetaPrograms/module_doc_no_lint.txt @@ -21,33 +21,35 @@ Physlib/Electromagnetism/FieldStrength/Basic.lean Physlib/Electromagnetism/FieldStrength/Derivative.lean Physlib/Electromagnetism/Homogeneous.lean Physlib/Electromagnetism/MaxwellEquations.lean +Physlib/Electromagnetism/Vacuum/Homogeneous.lean +Physlib/Electromagnetism/Vacuum/OneDimension.lean Physlib/Mathematics/Calculus/AdjFDeriv.lean Physlib/Mathematics/Calculus/Divergence.lean -Physlib/Mathematics/DataStructures/FourTree/Basic.lean -Physlib/Mathematics/DataStructures/FourTree/UniqueMap.lean -Physlib/Mathematics/DataStructures/Matrix/LieTrace.lean Physlib/Mathematics/Distribution/Basic.lean Physlib/Mathematics/Distribution/Function/InvPowMeasure.lean Physlib/Mathematics/Distribution/Function/IsDistBounded.lean Physlib/Mathematics/Distribution/Function/OfFunction.lean Physlib/Mathematics/Distribution/PowMul.lean -Physlib/Mathematics/FDerivCurry.lean -Physlib/Mathematics/Fin.lean -Physlib/Mathematics/Fin/Involutions.lean -Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean -Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean +Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean +Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean +Physlib/Mathematics/ForMathlib/DataStructures/Matrix/LieTrace.lean +Physlib/Mathematics/ForMathlib/FDerivCurry.lean +Physlib/Mathematics/ForMathlib/Fin.lean +Physlib/Mathematics/ForMathlib/Fin/Involutions.lean +Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean +Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean +Physlib/Mathematics/ForMathlib/LinearMaps.lean +Physlib/Mathematics/ForMathlib/List.lean +Physlib/Mathematics/ForMathlib/List/InsertIdx.lean +Physlib/Mathematics/ForMathlib/List/InsertionSort.lean +Physlib/Mathematics/ForMathlib/PiTensorProduct.lean +Physlib/Mathematics/ForMathlib/SchurTriangulation.lean +Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean Physlib/Mathematics/InnerProductSpace/Adjoint.lean Physlib/Mathematics/InnerProductSpace/Basic.lean Physlib/Mathematics/InnerProductSpace/Calculus.lean -Physlib/Mathematics/LinearMaps.lean -Physlib/Mathematics/List.lean -Physlib/Mathematics/List/InsertIdx.lean -Physlib/Mathematics/List/InsertionSort.lean -Physlib/Mathematics/PiTensorProduct.lean Physlib/Mathematics/SO3/Basic.lean -Physlib/Mathematics/SchurTriangulation.lean Physlib/Mathematics/SpecialFunctions/PhysHermite.lean -Physlib/Mathematics/Trigonometry/Tanh.lean Physlib/Mathematics/VariationalCalculus/Basic.lean Physlib/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean Physlib/Mathematics/VariationalCalculus/HasVarAdjoint.lean @@ -97,6 +99,7 @@ Physlib/Particles/FlavorPhysics/CKMMatrix/Relations.lean Physlib/Particles/FlavorPhysics/CKMMatrix/Rows.lean Physlib/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean Physlib/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean +Physlib/Particles/NeutrinoPhysics/Basic.lean Physlib/Particles/StandardModel/AnomalyCancellation/Basic.lean Physlib/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/Basic.lean @@ -190,6 +193,7 @@ Physlib/QuantumMechanics/OneDimension/GeneralPotential/Basic.lean Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Examples.lean Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean Physlib/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean Physlib/QuantumMechanics/OneDimension/HilbertSpace/Gaussians.lean @@ -311,7 +315,3 @@ Physlib/Units/WithDim/Momentum.lean Physlib/Units/WithDim/Pressure.lean Physlib/Units/WithDim/Speed.lean Physlib/Units/WithDim/Velocity.lean -Physlib/Electromagnetism/Vacuum/Homogeneous.lean -Physlib/Electromagnetism/Vacuum/OneDimension.lean -Physlib/Particles/NeutrinoPhysics/Basic.lean -Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Examples.lean From c7794ae30c8888f524f4d0d341a8e1e946e81f01 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:42:41 +0100 Subject: [PATCH 2/7] feat: Move SO3 file --- Physlib.lean | 2 +- Physlib/Mathematics/{ => Groups}/SO3/Basic.lean | 0 scripts/MetaPrograms/module_doc_no_lint.txt | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) rename Physlib/Mathematics/{ => Groups}/SO3/Basic.lean (100%) diff --git a/Physlib.lean b/Physlib.lean index d3511ffa09..1f976fe86d 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -143,6 +143,7 @@ public import Physlib.Mathematics.ForMathlib.Resolvent public import Physlib.Mathematics.ForMathlib.SchurTriangulation public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh +public import Physlib.Mathematics.Groups.SO3.Basic public import Physlib.Mathematics.InnerProductSpace.Adjoint public import Physlib.Mathematics.InnerProductSpace.Basic public import Physlib.Mathematics.InnerProductSpace.Calculus @@ -154,7 +155,6 @@ public import Physlib.Mathematics.LeviCivita.Basic public import Physlib.Mathematics.Modules.ConjModule public import Physlib.Mathematics.Modules.CrossProduct public import Physlib.Mathematics.Modules.CrossProductMatrix -public import Physlib.Mathematics.SO3.Basic public import Physlib.Mathematics.SpecialFunctions.EllipticIntegral public import Physlib.Mathematics.SpecialFunctions.PhysHermite public import Physlib.Mathematics.VariationalCalculus.Basic diff --git a/Physlib/Mathematics/SO3/Basic.lean b/Physlib/Mathematics/Groups/SO3/Basic.lean similarity index 100% rename from Physlib/Mathematics/SO3/Basic.lean rename to Physlib/Mathematics/Groups/SO3/Basic.lean diff --git a/scripts/MetaPrograms/module_doc_no_lint.txt b/scripts/MetaPrograms/module_doc_no_lint.txt index 4ed3350336..a7d316e859 100644 --- a/scripts/MetaPrograms/module_doc_no_lint.txt +++ b/scripts/MetaPrograms/module_doc_no_lint.txt @@ -45,10 +45,10 @@ Physlib/Mathematics/ForMathlib/List/InsertionSort.lean Physlib/Mathematics/ForMathlib/PiTensorProduct.lean Physlib/Mathematics/ForMathlib/SchurTriangulation.lean Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean +Physlib/Mathematics/Groups/SO3/Basic.lean Physlib/Mathematics/InnerProductSpace/Adjoint.lean Physlib/Mathematics/InnerProductSpace/Basic.lean Physlib/Mathematics/InnerProductSpace/Calculus.lean -Physlib/Mathematics/SO3/Basic.lean Physlib/Mathematics/SpecialFunctions/PhysHermite.lean Physlib/Mathematics/VariationalCalculus/Basic.lean Physlib/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean From 21adaaa745fcd1fb28b67f484ed2236b976c345e Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:43:15 +0100 Subject: [PATCH 3/7] feat: Add linters --- scripts/forMathlib_lint.lean | 111 +++++++++++++++++++++++++++++++++++ scripts/lint_all.lean | 4 ++ 2 files changed, 115 insertions(+) create mode 100644 scripts/forMathlib_lint.lean diff --git a/scripts/forMathlib_lint.lean b/scripts/forMathlib_lint.lean new file mode 100644 index 0000000000..021bcf635c --- /dev/null +++ b/scripts/forMathlib_lint.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import Lean +/-! + +# The `ForMathlib` linter + +The directory `Physlib/Mathematics/ForMathlib/` holds results which are not yet in Mathlib, and +are kept in Physlib only until they are upstreamed. This linter checks two properties of that +directory: + +1. No file in `ForMathlib` imports a module of `Physlib`, `PhyslibAlpha` or `QuantumInfo` from + outside `ForMathlib`. Imports from Mathlib, Batteries, Lean, etc. are allowed. This ensures that + every file in `ForMathlib` can be upstreamed without the rest of Physlib. +2. Every file in `ForMathlib` is used outside of `ForMathlib`: it is imported, either directly or + through other files in `ForMathlib`, by a file in `Physlib`, `PhyslibAlpha` or `QuantumInfo` + which is not itself in `ForMathlib`. The library root files such as `Physlib.lean` do not + count as uses. + +The linter only reads the import headers of files, so it does not need a build. + +It can be run from the terminal using +`lake exe forMathlib_lint`. + +-/ + +open Lean System + +/-- The module name prefix of the files in `Physlib/Mathematics/ForMathlib/`. -/ +def forMathlibPrefix : Name := `Physlib.Mathematics.ForMathlib + +/-- The library directories whose files are read by the linter. -/ +def libraryDirs : List String := ["Physlib", "PhyslibAlpha", "QuantumInfo"] + +/-- Whether a module lives in `Physlib/Mathematics/ForMathlib/`. -/ +def isForMathlib (n : Name) : Bool := forMathlibPrefix.isPrefixOf n + +/-- Whether a module lives in one of the libraries `Physlib`, `PhyslibAlpha` or `QuantumInfo`. -/ +def isLibraryModule (n : Name) : Bool := libraryDirs.any fun dir => dir.toName.isPrefixOf n + +/-- The module name of a `.lean` file, given its path relative to the repository root. -/ +def moduleNameOfPath (path : FilePath) : Name := + (path.withExtension "").components.foldl (fun n c => n.str c) .anonymous + +/-- The modules of `libraryDirs`, each paired with the modules of `libraryDirs` it imports. -/ +def libraryImports : IO (Array (Name × Array Name)) := do + let mut result := #[] + for dir in libraryDirs do + let paths ← FilePath.walkDir dir + for path in paths.filter (·.extension == some "lean") do + let contents ← IO.FS.readFile path + let (imports, _, _) ← Elab.parseImports contents path.toString + let libImports := (imports.map (·.module)).filter isLibraryModule + result := result.push (moduleNameOfPath path, libImports) + return result + +/-- The pairs `(m, i)` of a module `m` in `ForMathlib` importing a module `i` of `libraryDirs` + which is not in `ForMathlib`. -/ +def outsideImports (graph : Array (Name × Array Name)) : Array (Name × Name) := Id.run do + let mut result := #[] + for (m, imps) in graph.filter (isForMathlib ·.1) do + for i in imps.filter (! isForMathlib ·) do + result := result.push (m, i) + return result + +/-- The modules in `ForMathlib` which are not imported, directly or through other modules in + `ForMathlib`, by any module outside of `ForMathlib`. -/ +def unusedModules (graph : Array (Name × Array Name)) : Array Name := Id.run do + let importsOf : NameMap (Array Name) := + graph.foldl (fun acc (m, imps) => acc.insert m imps) {} + -- The modules in `ForMathlib` imported directly from outside of `ForMathlib`. + let mut todo : Array Name := #[] + for (_, imps) in graph.filter (! isForMathlib ·.1) do + todo := todo ++ imps.filter isForMathlib + -- Close under the imports of modules in `ForMathlib`. + let mut used : NameSet := {} + while h : todo.size > 0 do + let m := todo[todo.size - 1] + todo := todo.pop + unless used.contains m do + used := used.insert m + todo := todo ++ ((importsOf.find? m).getD #[]).filter isForMathlib + return (graph.map (·.1)).filter fun m => isForMathlib m && ! used.contains m + +/-- Sorts an array of names alphabetically. -/ +def sortNames (ns : Array Name) : Array Name := ns.qsort (·.toString < ·.toString) + +/-- Runs both checks, printing any violations, and returns `1` if there are any. -/ +def main : IO UInt32 := do + let graph ← libraryImports + let outside := (outsideImports graph).qsort fun a b => a.1.toString < b.1.toString + let unused := sortNames (unusedModules graph) + let forMathlibCount := (graph.filter (isForMathlib ·.1)).size + if outside.size > 0 then + IO.println s!"\x1b[31mError: Files in `{forMathlibPrefix}` must only import files \ + from within `{forMathlibPrefix}`:\x1b[0m" + for (m, i) in outside do + IO.println s!" {m} imports {i}" + if unused.size > 0 then + IO.println s!"\x1b[31mError: Files in `{forMathlibPrefix}` must be used outside of \ + `{forMathlibPrefix}`. The following are not:\x1b[0m" + for m in unused do + IO.println s!" {m}" + if outside.size > 0 || unused.size > 0 then + return 1 + IO.println s!"\x1b[32mAll {forMathlibCount} files in `{forMathlibPrefix}` import only from \ + `{forMathlibPrefix}` and are used outside of it.\x1b[0m" + return 0 diff --git a/scripts/lint_all.lean b/scripts/lint_all.lean index 2ab1d4879d..d0f9b004fa 100644 --- a/scripts/lint_all.lean +++ b/scripts/lint_all.lean @@ -32,6 +32,10 @@ def main (args : List String) : IO UInt32 := do let alphaFileImports ← IO.Process.output {cmd := "lake", args := #["exe", "alphaFileImports"]} println! alphaFileImports.stdout + println! "\x1b[36m(3/7) ForMathlib imports and uses\x1b[0m" + let forMathlibLint ← IO.Process.output {cmd := "lake", args := #["exe", "forMathlib_lint"]} + println! forMathlibLint.stdout + println! "\x1b[36m(4/7) TODO tag duplicates \x1b[0m" let todoCheck ← IO.Process.output {cmd := "lake", args := #["exe", "check_dup_tags"]} println! todoCheck.stdout From 8f5192b3b2b84e624b17fbef1ddca3bb51847c38 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:43:34 +0100 Subject: [PATCH 4/7] feat: Add linters --- lakefile.toml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/lakefile.toml b/lakefile.toml index 41c8a7ad47..4c6a2bc89c 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -85,6 +85,11 @@ name = "alphaFileImports" srcDir = "scripts/PhyslibAlpha" supportInterpreter = true +[[lean_exe]] +name = "forMathlib_lint" +srcDir = "scripts" +supportInterpreter = true + [[lean_exe]] name = "testImportScripts" srcDir = "Meta/test" From a8ce82917ca7a671d5d694952cb685edda947b35 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:44:17 +0100 Subject: [PATCH 5/7] feat: Remove linter errors --- Physlib.lean | 6 - .../DataStructures/FourTree/Basic.lean | 273 --------- .../DataStructures/FourTree/UniqueMap.lean | 228 ------- .../Metric/PseudoRiemannian/Defs.lean | 567 ------------------ .../Geometry/Metric/Riemannian/Defs.lean | 224 ------- .../Mathematics/ForMathlib/LinearMaps.lean | 3 - .../ForMathlib/PiTensorProduct.lean | 308 ---------- Physlib/Mathematics/ForMathlib/Resolvent.lean | 122 ---- Physlib/Meta/Linters/DefsWithUnderscore.lean | 3 +- Physlib/QFT/AnomalyCancellation/Basic.lean | 4 + scripts/MetaPrograms/module_doc_no_lint.txt | 5 - 11 files changed, 5 insertions(+), 1738 deletions(-) delete mode 100644 Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean delete mode 100644 Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean delete mode 100644 Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean delete mode 100644 Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean delete mode 100644 Physlib/Mathematics/ForMathlib/PiTensorProduct.lean delete mode 100644 Physlib/Mathematics/ForMathlib/Resolvent.lean diff --git a/Physlib.lean b/Physlib.lean index 1f976fe86d..70d996dc06 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -121,14 +121,10 @@ public import Physlib.Mathematics.Calculus.Wirtinger.Basic public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate public import Physlib.Mathematics.Distribution.Basic public import Physlib.Mathematics.Distribution.PowMul -public import Physlib.Mathematics.ForMathlib.DataStructures.FourTree.Basic -public import Physlib.Mathematics.ForMathlib.DataStructures.FourTree.UniqueMap public import Physlib.Mathematics.ForMathlib.DataStructures.Matrix.LieTrace public import Physlib.Mathematics.ForMathlib.FDerivCurry public import Physlib.Mathematics.ForMathlib.Fin public import Physlib.Mathematics.ForMathlib.Fin.Involutions -public import Physlib.Mathematics.ForMathlib.Geometry.Metric.PseudoRiemannian.Defs -public import Physlib.Mathematics.ForMathlib.Geometry.Metric.Riemannian.Defs public import Physlib.Mathematics.ForMathlib.HasTemperateGrowth public import Physlib.Mathematics.ForMathlib.LinearMaps public import Physlib.Mathematics.ForMathlib.LinearPMap @@ -138,8 +134,6 @@ public import Physlib.Mathematics.ForMathlib.List.InsertionSort public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Basic public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Unitary public import Physlib.Mathematics.ForMathlib.OrthogonalMatrix -public import Physlib.Mathematics.ForMathlib.PiTensorProduct -public import Physlib.Mathematics.ForMathlib.Resolvent public import Physlib.Mathematics.ForMathlib.SchurTriangulation public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh diff --git a/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean b/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean deleted file mode 100644 index 7df7a448a5..0000000000 --- a/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean +++ /dev/null @@ -1,273 +0,0 @@ -/- -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 - -public import Mathlib.Data.Multiset.Bind -public import Mathlib.Data.Multiset.Sort -/-! - -## The data type FourTree - -We define a tree-like structure, called `FourTree`, for storing values of a -type `α1 × α2 × α3 × α4`. - -It is defined recursively, with the following structure: -- A `leaf` contains a value of type `α4`. -- A `twig` contains a value of type `α3`, and a multiset of `leaf`s. -- A `branch` contains a value of type `α2`, and a multiset of `twig`s. -- A `trunk` contains a value of type `α1`, and a multiset of `branch`s. -- A `FourTree` contains a multiset of `trunk`s. - --/ - -@[expose] public section - -namespace Physlib - -namespace FourTree - -/-- A leaf contains has the data of a term of type `α4`. -/ -inductive Leaf (α4 : Type) - | leaf : α4 → Leaf α4 -deriving DecidableEq - -/-- A twig has the data of a term of type `α3` and a multiset of type `Leaf α4`. -/ -inductive Twig (α3 α4 : Type) - | twig : α3 → Multiset (Leaf α4) → Twig α3 α4 - -/-- A branch has the data of a term of type `α2` and a multiset of type `Twig α3 α4`. -/ -inductive Branch (α2 α3 α4 : Type) - | branch : α2 → Multiset (Twig α3 α4) → Branch α2 α3 α4 - -/-- A trunk has the data of a term of type `α1` and a multiset of type `Branch α2 α3 α4`. -/ -inductive Trunk (α1 α2 α3 α4 : Type) - | trunk : α1 → Multiset (Branch α2 α3 α4) → Trunk α1 α2 α3 α4 - -end FourTree - -/-- A `FourTree` has the data of a multiset of type `Trunk α1 α2 α3 α4`. -/ -inductive FourTree (α1 α2 α3 α4 : Type) - | root : Multiset (FourTree.Trunk α1 α2 α3 α4) → FourTree α1 α2 α3 α4 - -namespace FourTree - -open Leaf Twig Branch Trunk - -/-! - -## Repr instances for the FourTree - -These instances allow the `FourTree` to be printed in a human-readable format, -and copied and pasted. - --/ - -unsafe instance (α4 : Type) [Repr α4] : Repr (Leaf α4) where - reprPrec x _ := - match x with - | .leaf xs => "leaf " ++ reprStr xs - -unsafe instance (α3 α4 : Type) [Repr α3] [Repr α4] : Repr (Twig α3 α4) where - reprPrec x _ := - match x with - | .twig xs a => "twig " ++ reprStr xs ++ " " ++ reprStr a - -unsafe instance (α2 α3 α4: Type) [Repr α2] [Repr α3] [Repr α4] : - Repr (Branch α2 α3 α4) where - reprPrec x _ := - match x with - | .branch xa a => "branch (" ++ reprStr xa ++ ") " ++ reprStr a - -unsafe instance (α1 α2 α3 α4: Type) [Repr α1] [Repr α2] [Repr α3] [Repr α4] : - Repr (Trunk α1 α2 α3 α4) where - reprPrec x _ := - match x with - | .trunk xa a => "trunk (" ++ reprStr xa ++ ") " ++ reprStr a - -unsafe instance (α1 α2 α3 α4: Type) [Repr α1] [Repr α2] [Repr α3] [Repr α4] : - Repr (FourTree α1 α2 α3 α4) where - reprPrec x _ := - match x with - | .root xs => "root " ++ reprStr xs - -/-! - -## Conversion between FourTree and Multiset - --/ - -/-- A `FourTree` from a multiset of `α1 × α2 × α3 × α4`. -/ -def fromMultiset {α1 α2 α3 α4 : Type} [DecidableEq α1] - [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] - (l : Multiset (α1 × α2 × α3 × α4)) : FourTree α1 α2 α3 α4 := - let A1 : Multiset α1 := (l.map fun x => x.1).dedup - root <| A1.map fun xa => trunk xa <| - let B2 := (l.filter fun y => y.1 = xa) - let C2 : Multiset (α2 × α3 × α4) := (B2.map fun y => y.2).dedup - let A2 : Multiset α2 := (C2.map fun x => x.1).dedup - A2.map fun xb => branch xb <| - let B3 := (C2.filter fun y => y.1 = xb) - let C3 : Multiset (α3 × α4) := (B3.map fun y => y.2).dedup - let A3 : Multiset α3 := (C3.map fun x => x.1).dedup - A3.map fun xc => twig xc <| - let B4 := (C3.filter fun y => y.1 = xc) - let C4 : Multiset α4 := (B4.map fun y => y.2).dedup - C4.map fun xd => leaf xd - -/-- A `FourTree` to a multiset of `α1 × α2 × α3 × α4`. -/ -def toMultiset {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) : Multiset (α1 × α2 × α3 × α4) := - match T with - | .root trunks => - trunks.bind fun (trunk xT branches) => - branches.bind fun (branch xB twigs) => - twigs.bind fun (twig xTw leafs) => - leafs.map fun (leaf xL) => (xT, xB, xTw, xL) - -/-! - -## Cardinality of the tree - --/ - -/-- The cardinality of a `Twig` is the number of leafs. -/ -def Twig.card {α3 α4 : Type} (T : Twig α3 α4) : Nat := - match T with - | .twig _ leafs => leafs.card - -/-- The cardinality of a `Branch` is the total number of leafs. -/ -def Branch.card {α2 α3 α4 : Type} (T : Branch α2 α3 α4) : Nat := - match T with - | .branch _ twigs => (twigs.map Twig.card).sum - -/-- The cardinality of a `Trunk` is the total number of leafs. -/ -def Trunk.card {α1 α2 α3 α4 : Type} (T : Trunk α1 α2 α3 α4) : Nat := - match T with - | .trunk _ branches => (branches.map Branch.card).sum - -/-- The cardinality of a `FourTree` is the total number of leafs. -/ -def card {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) : Nat := - match T with - | .root trunks => (trunks.map Trunk.card).sum - -lemma card_eq_toMultiset_card (T : FourTree α1 α2 α3 α4s) : - T.card = T.toMultiset.card := by - simp only [card, toMultiset, Multiset.card_bind, Function.comp_apply, Multiset.card_map] - rfl - -/-! - -## Membership of a FourTree - -Based on the tree structure we can define a faster membership criterion, which -is equivalent to membership based on multisets. - --/ - -variable {α1 α2 α3 α4 : Type} - -/-- An element of `a : α4` is a member of `Leaf α4` if the underlying element of the `Leaf` - is `a`. -/ -def Leaf.mem {α4} (T : Leaf α4) (x : α4) : Prop := - match T with - | .leaf xs => xs = x - -instance {α4} [DecidableEq α4] (T : Leaf α4) (x : α4) : Decidable (T.mem x) := - inferInstanceAs (Decidable (match T with | .leaf xs => xs = x)) - -/-- An element of `a : α3 × α4` is a member of `Twig α3 α4` if the underlying `α3` element of the - `Twig` is `a.1` and `a.2` is a member of one of the `Leaf`. -/ -def Twig.mem (T : Twig α3 α4) (x : α3 × α4) : Prop := - match T with - | .twig xs leafs => xs = x.1 ∧ ∃ leaf ∈ leafs, leaf.mem x.2 - -instance {α3 α4} [DecidableEq α3] [DecidableEq α4] (T : Twig α3 α4) (x : α3 × α4) : - Decidable (T.mem x) := - match T with - | .twig _ leafs => - haveI : Decidable (∃ leaf ∈ leafs, leaf.mem x.2) := Multiset.decidableExistsMultiset - instDecidableAnd - -/-- An element of `a : α2 × α3 × α4` is a member of `Branch α2 α3 α4` if the underlying `α2` - element of the `Branch` is `a.1` and `a.2` is a member of one of the `Twig`. -/ -def Branch.mem (T : Branch α2 α3 α4) (x : α2 × α3 × α4) : Prop := - match T with - | .branch xo twigs => xo = x.1 ∧ ∃ twig ∈ twigs, twig.mem x.2 - -instance [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (T : Branch α2 α3 α4) - (x : α2 × α3 × α4) : Decidable (T.mem x) := - match T with - | .branch _ twigs => - haveI : Decidable (∃ twig ∈ twigs, twig.mem x.2) := Multiset.decidableExistsMultiset - instDecidableAnd - -/-- An element of `a : α1 × α2 × α3 × α4` is a member of `Trunk α1 α2 α3 α4` if the underlying `α1` - element of the `Trunk` is `a.1` and `a.2` is a member of one of the `Branch`. -/ -def Trunk.mem (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop := - match T with - | .trunk xo branches => xo = x.1 ∧ ∃ branch ∈ branches, branch.mem x.2 - -instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] - (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x) := - match T with - | .trunk _ branches => - haveI : Decidable (∃ branch ∈ branches, branch.mem x.2) := Multiset.decidableExistsMultiset - instDecidableAnd - -/-- An element of `a : α1 × α2 × α3 × α4` is a member of `FourTree α1 α2 α3 α4` if - `a` is a member of one of the `Trunk`. -/ -def mem (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop := - match T with - | .root trunks => ∃ trunk ∈ trunks, trunk.mem x - -instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] - (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x) := - Multiset.decidableExistsMultiset - -instance : Membership (α1 × α2 × α3 × α4) (FourTree α1 α2 α3 α4) where - mem := mem - -instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] - (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (x ∈ T) := - Multiset.decidableExistsMultiset - -lemma mem_iff_mem_toMultiset (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : - x ∈ T ↔ x ∈ T.toMultiset := by - have leaf_iff : ∀ (l : Leaf α4) (y : α4), l.mem y ↔ l.1 = y := by - rintro ⟨_⟩ _ - rfl - have twig_iff : ∀ (t : Twig α3 α4) (y : α3 × α4), - t.mem y ↔ t.1 = y.1 ∧ ∃ l ∈ t.2, l.mem y.2 := by - rintro ⟨_, _⟩ _ - rfl - have branch_iff : ∀ (b : Branch α2 α3 α4) (y : α2 × α3 × α4), - b.mem y ↔ b.1 = y.1 ∧ ∃ t ∈ b.2, t.mem y.2 := by - rintro ⟨_, _⟩ _ - rfl - have trunk_iff : ∀ (k : Trunk α1 α2 α3 α4) (y : α1 × α2 × α3 × α4), - k.mem y ↔ k.1 = y.1 ∧ ∃ b ∈ k.2, b.mem y.2 := by - rintro ⟨_, _⟩ _ - rfl - obtain ⟨trunks⟩ := T - show (∃ trunk ∈ trunks, trunk.mem x) ↔ x ∈ (root trunks).toMultiset - simp only [toMultiset, Multiset.mem_bind, Multiset.mem_map, - trunk_iff, branch_iff, twig_iff, leaf_iff, Prod.ext_iff] - tauto - -lemma mem_of_parts {T : FourTree α1 α2 α3 α4} {C : α1 × α2 × α3 × α4} - (trunk : Trunk α1 α2 α3 α4) - (branch : Branch α2 α3 α4) - (twig : Twig α3 α4) (leaf : Leaf α4) - (trunk_mem : trunk ∈ T.1) (branch_mem : branch ∈ trunk.2) - (twig_mem : twig ∈ branch.2) (leaf_mem : leaf ∈ twig.2) - (heq : C = (trunk.1, branch.1, twig.1, leaf.1)) : - C ∈ T := by - rw [mem_iff_mem_toMultiset] - simp only [toMultiset, Multiset.mem_bind, Multiset.mem_map] - exact ⟨trunk, trunk_mem, branch, branch_mem, twig, twig_mem, leaf, leaf_mem, heq.symm⟩ - -end FourTree - -end Physlib diff --git a/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean b/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean deleted file mode 100644 index a92042f67f..0000000000 --- a/Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean +++ /dev/null @@ -1,228 +0,0 @@ -/- -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 - -public import Physlib.Mathematics.ForMathlib.DataStructures.FourTree.Basic -/-! - -## Unique maps for `FourTree` - -We define the `uniqueMap4` and `uniqueMap3` functions for `FourTree`. -For a given `f : α4 → α4` or `f : α3 → α3`, these functions the elements of a `FourTree`, -and leave only new elements which are not already present in the tree (if -the tree has no duplicates). - --/ - -@[expose] public section - -namespace Physlib - -namespace FourTree - -/-! - -## uniqueMap4 - --/ - -section uniqueMap4 - -variable {α1 α2 α3 α4 : Type} [DecidableEq α4] (f : α4 → α4) - -/-- Given a map `f : α4 → α4` the map from `Leaf α4 → Leaf α4` mapping the underlying - elements. -/ -def Leaf.uniqueMap4 : Leaf α4 → Leaf α4 - | .leaf x => .leaf (f x) - -/-- Given a map `f : α4 → α4` the map from `Twig α3 α4 → Twig α3 α4` mapping the underlying - leafs and deleting any that appear in the original Twig. -/ -def Twig.uniqueMap4 (T : Twig α3 α4) : Twig α3 α4 := - match T with - | .twig xs leafs => - let leafFinst := leafs.map (fun l => match l with - | .leaf ys => ys) - let sub : Multiset α4 := leafFinst.filterMap (fun ys => - if ¬ f ys ∈ leafFinst then - some (f ys) - else - none) - .twig xs (sub.map (fun ys => .leaf ys)) - -/-- Given a map `f : α4 → α4` the map from `Branch α2 α3 α4 → Branch α2 α3 α4` - mapping the underlying leafs and deleting any that appear in the original Twig. -/ -def Branch.uniqueMap4 (T : Branch α2 α3 α4) : - Branch α2 α3 α4:= - match T with - | .branch xo twigs => - .branch xo (twigs.map fun ts => (Twig.uniqueMap4 f ts)) - -/-- Given a map `f : α4 → α4` the map from `Trunk α1 α2 α3 α4 → Trunk α1 α2 α3 α4` - mapping the underlying leafs and deleting any that appear in the original Twig. -/ -def Trunk.uniqueMap4 (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4 := - match T with - | .trunk xo branches => - .trunk xo (branches.map fun bs => (Branch.uniqueMap4 f bs)) - -/-- Given a map `f : α4 → α4` the map from `FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4` - mapping the underlying leafs and deleting any that appear in the original twig of that - leaf. -/ -def uniqueMap4 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4 := - match T with - | .root trunks => - .root (trunks.map fun ts => (ts.uniqueMap4 f)) - -lemma map_mem_uniqueMap4 {T : FourTree α1 α2 α3 α4} - (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α4 → α4) : - (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T.uniqueMap4 f ∨ - (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T := by - by_cases hnotMem : (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T - · simp [hnotMem] - left - simp [mem_iff_mem_toMultiset, toMultiset] at hx - obtain ⟨trunk, htrunk, branch, hbranch, twig, htwig, leaf, hleaf, heq⟩ := hx - apply mem_of_parts (trunk.uniqueMap4 f) (branch.uniqueMap4 f) (twig.uniqueMap4 f) - (.leaf (f leaf.1)) - · exact Multiset.mem_map_of_mem _ htrunk - · exact Multiset.mem_map_of_mem _ hbranch - · exact Multiset.mem_map_of_mem _ htwig - · simp [Twig.uniqueMap4, -existsAndEq] - refine ⟨leaf, hleaf, ?_, rfl⟩ - intro y hy hn - exact hnotMem - (mem_of_parts trunk branch twig y htrunk hbranch htwig hy (by subst heq; simp [hn])) - · subst heq - simp [Trunk.uniqueMap4, Branch.uniqueMap4, Twig.uniqueMap4] - -lemma exists_of_mem_uniqueMap4 {T : FourTree α1 α2 α3 α4} - (C : α1 × α2 × α3 × α4) (h : C ∈ T.uniqueMap4 f) : - ∃ qHd qHu Q5 Q10, C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T := by - rw [mem_iff_mem_toMultiset] at h - simp [toMultiset] at h - obtain ⟨trunkI, trunkI_mem, branchI, branchI_mem, twigI, twigI_mem, - leafI, leafI_mem, heq⟩ := h - -- obtaining trunkT - simp [uniqueMap4] at trunkI_mem - obtain ⟨trunkT, trunkT_mem, rfl⟩ := trunkI_mem - -- obtaining branchT - simp [Trunk.uniqueMap4] at branchI_mem - obtain ⟨branchT, branchT_mem, rfl⟩ := branchI_mem - -- obtaining twigT - simp only [Branch.uniqueMap4, Multiset.mem_map] at twigI_mem - obtain ⟨twigT, twigT_mem, rfl⟩ := twigI_mem - -- obtaining leafT - simp only [Twig.uniqueMap4, Multiset.mem_map, Multiset.mem_filterMap, - Option.ite_none_right_eq_some, Option.some.injEq, exists_exists_and_eq_and] at leafI_mem - obtain ⟨Q10, ⟨leafT, leafT_mem, hQ10⟩, hPresent⟩ := leafI_mem - subst heq - refine ⟨trunkT.1, branchT.1, twigT.1, leafT.1, ?_, - mem_of_parts trunkT branchT twigT leafT trunkT_mem branchT_mem twigT_mem leafT_mem rfl⟩ - rw [← hPresent] - simp [Trunk.uniqueMap4, Branch.uniqueMap4, Twig.uniqueMap4, hQ10.2] - -end uniqueMap4 - -/-! - -## uniqueMap3 - --/ - -section uniqueMap3 - -variable {α1 α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (f : α3 → α3) - -/-- Given a map `f : α3 → α3` the map from `Twig α3 α4 → Twig α3 α4` mapping the underlying - first value of the twig. -/ -def Twig.uniqueMap3 (T : Twig α3 α4) : Twig α3 α4 := - match T with - | .twig xs leafs => .twig (f xs) leafs - -/-- Given a map `f : α3 → α3` the map from `Branch α2 α3 α4 → Branch α2 α3 α4` mapping the - underlying first value of the twig, and deleting any new leafs that appeared - in the old branch. -/ -def Branch.uniqueMap3 (T : Branch α2 α3 α4) : Branch α2 α3 α4 := - match T with - | .branch qHu twigs => - let insertTwigs := twigs.map (fun (.twig Q5 leafs) => Twig.twig (f Q5) - (leafs.filter (fun (.leaf Q10) => ¬ Branch.mem (.branch qHu twigs) - (qHu, (f Q5), Q10)))) - .branch qHu insertTwigs - -/-- Given a map `f : α3 → α3` the map from `Trunk α1 α2 α3 α4 → Trunk α1 α2 α3 α4` mapping the - underlying first value of the twig, and deleting any new leafs that appeared - in the old branch. -/ -def Trunk.uniqueMap3 (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4 := - match T with - | .trunk qHd branches => - .trunk qHd (branches.map fun bs => (bs.uniqueMap3 f)) - -/-- Given a map `f : α3 → α3` the map from `FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4` mapping the - underlying first value of the twig, and deleting any new leafs that appeared - in the old branch. -/ -def uniqueMap3 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4:= - match T with - | .root trunks => - .root (trunks.map fun ts => (ts.uniqueMap3 f)) - -lemma map_mem_uniqueMap3 {T : FourTree α1 α2 α3 α4} - (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α3 → α3) : - (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T.uniqueMap3 f ∨ - (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T := by - by_cases hnotMem : (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T - · simp [hnotMem] - left - simp [mem_iff_mem_toMultiset, toMultiset] at hx - obtain ⟨trunk, htrunk, branch, hbranch, twig, htwig, leaf, hleaf, heq⟩ := hx - match branch with - | .branch qHu twigs => - match twig with - | .twig Q5 leafs => - apply mem_of_parts (trunk.uniqueMap3 f) ((Branch.branch qHu twigs).uniqueMap3 f) - (.twig (f Q5) (leafs.filter (fun (.leaf Q10) => - ¬ Branch.mem (.branch qHu twigs) (qHu, f Q5, Q10)))) leaf - · exact Multiset.mem_map_of_mem _ htrunk - · exact Multiset.mem_map_of_mem _ hbranch - · exact Multiset.mem_map_of_mem _ htwig - · refine Multiset.mem_filter.mpr ⟨hleaf, ?_⟩ - show ¬ (Branch.branch qHu twigs).mem (qHu, f Q5, leaf.1) - by_contra hn - apply hnotMem - subst heq - exact ⟨trunk, htrunk, rfl, .branch qHu twigs, hbranch, hn⟩ - · subst heq - simp [Trunk.uniqueMap3, Branch.uniqueMap3] - -lemma exists_of_mem_uniqueMap3 {T : FourTree α1 α2 α3 α4} - (C : α1 × α2 × α3 × α4) (h : C ∈ T.uniqueMap3 f) : - ∃ qHd qHu Q5 Q10, C = (qHd, qHu, f Q5, Q10) ∧ - (qHd, qHu, Q5, Q10) ∈ T := by - rw [mem_iff_mem_toMultiset] at h - simp [toMultiset] at h - obtain ⟨trunkI, trunkI_mem, branchI, branchI_mem, twigI, twigI_mem, - leafI, leafI_mem, heq⟩ := h - -- obtaining trunkT - simp [uniqueMap3] at trunkI_mem - obtain ⟨trunkT, trunkT_mem, rfl⟩ := trunkI_mem - -- obtaining branchT - simp [Trunk.uniqueMap3] at branchI_mem - obtain ⟨branchT, branchT_mem, rfl⟩ := branchI_mem - -- obtaining twigT - simp only [Branch.uniqueMap3, Multiset.mem_map] at twigI_mem - obtain ⟨twigT, twigT_mem, rfl⟩ := twigI_mem - -- obtaining leafT - simp at leafI_mem - obtain ⟨leftI_mem, h_not_mem⟩ := leafI_mem - subst heq - refine ⟨trunkT.1, branchT.1, twigT.1, leafI.1, ?_, - mem_of_parts trunkT branchT twigT leafI trunkT_mem branchT_mem twigT_mem leftI_mem rfl⟩ - simp [Trunk.uniqueMap3, Branch.uniqueMap3] - -end uniqueMap3 - -end FourTree - -end Physlib diff --git a/Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean b/Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean deleted file mode 100644 index aa6de38d2a..0000000000 --- a/Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean +++ /dev/null @@ -1,567 +0,0 @@ -/- -Copyright (c) 2025 Matteo Cipollina. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Matteo Cipollina --/ -module - -public import Mathlib.Analysis.InnerProductSpace.Basic -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 - -This file formalizes pseudo-Riemannian metrics on smooth manifolds and establishes their basic -properties. - -A pseudo-Riemannian metric equips a manifold with a smoothly varying, non-degenerate, symmetric -bilinear form of *constant index* on each tangent space, generalizing the concept of an inner -product space to curved spaces. The index here refers to `QuadraticForm.negDim`, the dimension -of a maximal negative definite subspace. - -## Main Definitions - -* `PseudoRiemannianMetric E H M n I`: A structure representing a `C^n` pseudo-Riemannian metric - on a manifold `M` modelled on `(E, H)` with model with corners `I`. It consists of a family - of non-degenerate, symmetric, continuous bilinear forms `gₓ` on each tangent space `TₓM`, - varying `C^n`-smoothly with `x` and having a locally constant negative dimension (`negDim`). - The model space `E` must be finite-dimensional, and the manifold `M` must be `C^{n+1}` smooth. - -* `PseudoRiemannianMetric.flatEquiv g x`: The "musical isomorphism" from the tangent space at `x` - to its dual space, representing the canonical isomorphism induced by the metric. - -* `PseudoRiemannianMetric.sharpEquiv g x`: The inverse of the flat isomorphism, mapping from - the dual space back to the tangent space. - -* `PseudoRiemannianMetric.toQuadraticForm g x`: The quadratic form `v ↦ gₓ(v, v)` associated - with the metric at point `x`. - -This formalization adopts a direct approach, defining the metric as a family of bilinear forms -on tangent spaces, varying smoothly over the manifold. This pragmatic choice allows for foundational -development while acknowledging that a more abstract ideal would involve defining metrics as -sections of a tensor bundle (e.g., `Hom(TM ⊗ TM, ℝ)` or `TM →L[ℝ] TM →L[ℝ] ℝ`. - -## References - -* Barrett O'Neill, Semi-Riemannian Geometry With Applications to Relativity, Academic Press, 1983. - [ref: oneill_1983_semi_riemannian] -* Discussion on Zulip about (Pseudo) Riemannian metrics: - https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.28Pseudo.29.20Riemannian.20metric --/ - -@[expose] public section - -section PseudoRiemannianMetric - -noncomputable section - -open Bundle Set Finset Function Filter Module Topology ContinuousLinearMap -open scoped Manifold Bundle LinearMap Dual - -namespace QuadraticForm - -variable {K : Type*} [Field K] - -/-! ## Negative Index -/ - -/-- The negative dimension (often called the index or negative index of inertia) of a -quadratic form `q` on a finite-dimensional real vector space. - -This value is defined by diagonalizing the quadratic form into an equivalent -`QuadraticMap.weightedSumSquares ℝ s`, where `s : Fin (finrank ℝ E) → SignType` -assigns `1`, `0`, or `-1` to each component. The `negDim` is the count of -components `i` for which `s i = SignType.neg`. - -By Sylvester's Law of Inertia, this count is an invariant of the quadratic form. -Geometrically, `negDim q` represents the dimension of any maximal vector subspace -on which `q` is negative definite. This corresponds to O'Neill's Definition 18 (p. 47) -of the index `ν` of a symmetric bilinear form `b` on `V`, which is "the largest integer -that is the dimension of a subspace `W ⊂ V` on which `b|W` is negative -definite." -/ -noncomputable def negDim {E : Type*} [AddCommGroup E] - [Module ℝ E] [FiniteDimensional ℝ E] - (q : QuadraticForm ℝ E) : ℕ := by classical - let P : (Fin (finrank ℝ E) → SignType) → Prop := fun w => - QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ)) - let h_exists : ∃ w, P w := QuadraticForm.equivalent_signType_weighted_sum_squared q - let w := Classical.choose h_exists - exact Finset.card (Finset.filter (fun i => w i = SignType.neg) Finset.univ) - -/-- For a standard basis vector in a weighted sum of squares, only one term in the sum - is nonzero. -/ -lemma QuadraticMap.weightedSumSquares_basis_vector {E : Type*} [AddCommGroup E] - [Module ℝ E] {weights : Fin (finrank ℝ E) → ℝ} - {i : Fin (finrank ℝ E)} (v : Fin (finrank ℝ E) → ℝ) - (hv : ∀ j, v j = if j = i then 1 else 0) : - QuadraticMap.weightedSumSquares ℝ weights v = weights i := by - rw [QuadraticMap.weightedSumSquares_apply, Finset.sum_eq_single_of_mem i (mem_univ i)] - · simp [hv i] - · intro j _ hj - simp [hv j, hj] - -/-- When a quadratic form is equivalent to a weighted sum of squares, - negative weights correspond to vectors where the form takes negative values. - This is a concrete realization of a 1-dimensional negative definite subspace, - contributing to O'Neill's index `ν` (Definition 18, p. 47). -/ -lemma neg_weight_implies_neg_value {E : Type*} [AddCommGroup E] [Module ℝ E] - {q : QuadraticForm ℝ E} {w : Fin (finrank ℝ E) → SignType} - (h_equiv : QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ))) - {i : Fin (finrank ℝ E)} (hi : w i = SignType.neg) : - ∃ v : E, v ≠ 0 ∧ q v < 0 := by - let f := Classical.choice h_equiv - let v_std : Fin (finrank ℝ E) → ℝ := fun j => if j = i then 1 else 0 - refine ⟨f.symm v_std, ?_, ?_⟩ - · intro h - have hz : v_std = 0 := by - have hf := congrArg f h - rwa [f.apply_symm_apply, map_zero] at hf - simpa [v_std] using congrFun hz i - · have hw : QuadraticMap.weightedSumSquares ℝ (fun j => (w j : ℝ)) v_std = (w i : ℝ) := - QuadraticMap.weightedSumSquares_basis_vector v_std fun _ => rfl - rw [QuadraticMap.IsometryEquiv.map_app f.symm v_std, hw, hi, SignType.neg_eq_neg_one, - SignType.coe_neg, SignType.coe_one] - norm_num - -/-- A positive definite quadratic form cannot have any negative weights - in its diagonal representation. A quadratic form `q` derived from a bilinear form `b` - is positive definite if `b(v,v) > 0` for `v ≠ 0` (O'Neill, Definition 17 (1), p. 46). - The existence of a negative weight would imply `q(v) < 0` for some `v ≠ 0`, a contradiction. -/ -lemma posDef_no_neg_weights {E : Type*} [AddCommGroup E] [Module ℝ E] - {q : QuadraticForm ℝ E} (hq : q.PosDef) - {w : Fin (finrank ℝ E) → SignType} - (h_equiv : QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ))) : - ∀ i, w i ≠ SignType.neg := by - intro i hi - obtain ⟨v, hv, hq_neg⟩ := QuadraticForm.neg_weight_implies_neg_value h_equiv hi - exact lt_asymm hq_neg (hq v hv) - -/-- For a positive definite quadratic form, the negative dimension (index) is zero. - O'Neill states (p. 47) that "ν = 0 if and only if b is positive semidefinite." - Since positive definite implies positive semidefinite (Definitions 17 (1) and (2), p. 46), - a positive definite form must have index `ν = 0`. -/ -theorem rankNeg_eq_zero {E : Type*} [AddCommGroup E] - [Module ℝ E] [FiniteDimensional ℝ E] {q : QuadraticForm ℝ E} (hq : q.PosDef) : - q.negDim = 0 := by - have : Invertible (2 : ℝ) := inferInstance - unfold QuadraticForm.negDim - have h_exists := equivalent_signType_weighted_sum_squared q - let w := Classical.choose h_exists - have h_no_neg : ∀ i, w i ≠ SignType.neg := - QuadraticForm.posDef_no_neg_weights hq (Classical.choose_spec h_exists) - simpa [Finset.card_eq_zero, Finset.filter_eq_empty_iff] using h_no_neg - -end QuadraticForm - -/-! ## Pseudo-Riemannian Metric -/ - -/-- -Constructs a `QuadraticForm` on the tangent space `TₓM` at a point `x` from the -value of a pseudo-Riemannian metric at that point. -(O'Neill, p. 47, "The function q: V → R given by q(v) = b(v,v) is the associated quadratic -form of b.") -The pseudo-Riemannian metric is given by `val`, a family of continuous bilinear forms -`gₓ: TₓM × TₓM → ℝ` for each `x : M`. -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)`. --/ -def pseudoRiemannianMetricValToQuadraticForm - {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] - {H : Type w} [TopologicalSpace H] - {M : Type w} [TopologicalSpace M] [ChartedSpace H M] - {I : ModelWithCorners ℝ E H} - (val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) - (symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v) - (x : M) : QuadraticForm ℝ (TangentSpace I x) where - toFun v := val x v v - toFun_smul a v := by - simp only [ContinuousLinearMap.map_smul, _root_.smul_apply, smul_smul] - exists_companion' := - ⟨LinearMap.mk₂ ℝ (fun v y => val x v y + val x y v) - (fun v₁ v₂ y => by simp only [map_add, add_apply]; ring) - (fun a v y => by simp only [map_smul, smul_apply]; ring) - (fun v y₁ y₂ => by simp only [map_add, add_apply]; ring) - (fun a v y => by simp only [map_smul, smul_apply]; ring), - by - intro v y - simp only [LinearMap.mk₂_apply, ContinuousLinearMap.map_add, - add_apply, symm x] - ring⟩ - -/-- A pseudo-Riemannian metric of smoothness class `C^n` on a manifold `M` modelled on `(E, H)` -with model `I`. This structure defines a smoothly varying, non-degenerate, symmetric, -continuous bilinear form `gₓ` of constant negative dimension on the tangent space `TₓM` -at each point `x`. Requires `M` to be `C^{n+1}` smooth. -This structure formalizes O'Neill's Definition 3.1 (p. 54) of a metric tensor `g` on `M` -as a "symmetric non-degenerate (0,2) tensor field on M of constant index." -Each `gₓ` is a scalar product (O'Neill, Definition 20, p. 47) on `TₓM`. -/ -@[ext] -structure PseudoRiemannianMetric - (E : Type v) (H : Type w) (M : Type w) (n : WithTop ℕ∞) - [inst_norm_grp_E : NormedAddCommGroup E] - [inst_norm_sp_E : NormedSpace ℝ E] - [inst_top_H : TopologicalSpace H] - [inst_top_M : TopologicalSpace M] - [inst_chart_M : ChartedSpace H M] - [inst_chart_E : ChartedSpace H E] - (I : ModelWithCorners ℝ E H) - [inst_mani : IsManifold I (n + 1) M] - [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] : - Type (max u v w) where - /-- The metric tensor at each point `x : M`, represented as a continuous linear map - `TₓM →L[ℝ] (TₓM →L[ℝ] ℝ)`. Applying it twice, `(val x v) w`, yields `gₓ(v, w)`. -/ - val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) - /-- The metric is symmetric: `gₓ(v, w) = gₓ(w, v)`. -/ - symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v - /-- The metric is non-degenerate: if `gₓ(v, w) = 0` for all `w`, then `v = 0`. -/ - nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ w : TangentSpace I x, - (val x v) w = 0) → v = 0 - /-- The metric varies smoothly: Expressed in local coordinates via the chart - `e := extChartAt I x₀`, the function - `y ↦ g_{e.symm y}(mfderiv I I e.symm y v, mfderiv I I e.symm y w)` is `C^n` smooth on the - chart's target `e.target` for any constant vectors `v, w` in the model space `E`. -/ - smooth_in_charts' : ∀ (x₀ : M) (v w : E), - let e := extChartAt I x₀ - ContDiffWithinAt ℝ n - (fun y => val (e.symm y) (mfderiv I I e.symm y v) (mfderiv I I e.symm y w)) - (e.target) (e x₀) - /-- The negative dimension (`QuadraticForm.negDim`) of the metric's quadratic form is - locally constant. On a connected manifold, this implies it is constant globally. -/ - negDim_isLocallyConstant : - IsLocallyConstant (fun x : M => - have : FiniteDimensional ℝ (TangentSpace I x) := inferInstance - (pseudoRiemannianMetricValToQuadraticForm val symm x).negDim) - -namespace PseudoRiemannianMetric - -variable {E : Type v} {H : Type w} {M : Type w} {n : WithTop ℕ∞} -variable [NormedAddCommGroup E] [NormedSpace ℝ E] -variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E] -variable {I : ModelWithCorners ℝ E H} -variable [IsManifold I (n + 1) M] -variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] -variable {g : PseudoRiemannianMetric E H M n I} - -/-- Given a pseudo-Riemannian metric `g` on manifold `M` and a point `x : M`, -this function constructs a bilinear form on the tangent space at `x`. -For tangent vectors `u v : T_x M`, the bilinear form is given by: -`g_x(u, v) = g(x)(u, v)` -/ -def toBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - LinearMap.BilinForm ℝ (TangentSpace I x) where - toFun := λ v => { toFun := λ w => g.val x v w, - map_add' := λ w₁ w₂ => by - simp only [ContinuousLinearMap.map_add], - map_smul' := λ c w => by - simp only [map_smul, smul_eq_mul, RingHom.id_apply] } - map_add' := λ v₁ v₂ => by - ext w - simp only [map_add, add_apply, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] - map_smul' := λ c v => by - ext w - simp only [map_smul, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul, LinearMap.coe_mk, - AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply] - -/-- Convert a pseudo-Riemannian metric at a point `x` to a quadratic form `v ↦ gₓ(v, v)`. -/ -abbrev toQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - QuadraticForm ℝ (TangentSpace I x) := - pseudoRiemannianMetricValToQuadraticForm g.val g.symm x - -/-- Coercion from PseudoRiemannianMetric to its function representation. -/ -instance coeFunInst : CoeFun (PseudoRiemannianMetric E H M n I) - (fun _ => ∀ x : M, TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) where - coe g := g.val - -@[simp] -lemma toBilinForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (v w : TangentSpace I x) : - toBilinForm g x v w = g.val x v w := rfl - -@[simp] -lemma toQuadraticForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (v : TangentSpace I x) : - toQuadraticForm g x v = g.val x v v := rfl - -@[simp] -lemma toBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) : - (toBilinForm g x).IsSymm := ⟨g.symm x⟩ - -@[simp] -lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : - (toBilinForm g x).Nondegenerate := by - refine ⟨fun v hv => g.nondegenerate x v hv, fun v hv => ?_⟩ - exact g.nondegenerate x v fun w => (g.symm x v w).trans (hv w) - -/-- The inner product (or scalar product) on the tangent space at point `x` - induced by the pseudo-Riemannian metric `g`. This is `gₓ(v, w)`. -/ -def inner (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : ℝ := - g.val x v w - -@[simp] -lemma inner_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - inner g x v w = g.val x v w := rfl - -/-! ## Flat -/ - -section Flat - -/-- The "musical" isomorphism (index lowering) `v ↦ gₓ(v, -)`. -The non-degeneracy of `gₓ` (O'Neill, Def 17 (3), p. 46) means its matrix representation -is invertible (O'Neill, Lemma 19, p. 47), and that this map is an isomorphism from `TₓM` -to its dual. -/ -def flat (g : PseudoRiemannianMetric E H M n I) (x : M) : - TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) := - { toFun := λ v => g.val x v, - map_add' := λ v w => by simp only [ContinuousLinearMap.map_add], - map_smul' := λ a v => by simp only [ContinuousLinearMap.map_smul]; rfl } - -@[simp] -lemma flat_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - (flat g x v) w = g.val x v w := by rfl - -/-- The musical isomorphism as a continuous linear map. -/ -def flatL (g : PseudoRiemannianMetric E H M n I) (x : M) : - TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) where - toFun := λ v => g.val x v - map_add' := λ v w => by simp only [ContinuousLinearMap.map_add] - map_smul' := λ a v => by simp only [ContinuousLinearMap.map_smul]; rfl - cont := ContinuousLinearMap.continuous (g.val x) - -@[simp] -lemma flatL_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - (flatL g x v) w = g.val x v w := rfl - -@[simp] -lemma flat_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Injective (flat g x) := by - rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'] - exact fun v hv => g.nondegenerate x v fun w => DFunLike.congr_fun hv w - -@[simp] -lemma flatL_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Injective (flatL g x) := - flat_inj g x - -@[simp] -lemma flatL_surj - (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Surjective (g.flatL x) := by - have : FiniteDimensional ℝ (TangentSpace I x) := inst_tangent_findim x - have : T2Space (TangentSpace I x) := inferInstanceAs (T2Space E) - have h_finrank_eq : finrank ℝ (TangentSpace I x) = finrank ℝ (TangentSpace I x →L[ℝ] ℝ) := - Subspace.dual_finrank_eq.symm.trans (LinearMap.toContinuousLinearMap - (𝕜 := ℝ) (E := TangentSpace I x) (F' := ℝ)).finrank_eq - exact (LinearMap.injective_iff_surjective_of_finrank_eq_finrank h_finrank_eq).mp (flatL_inj g x) - -/-- The "musical" isomorphism (index lowering) from `TₓM` to its dual, -as a continuous linear equivalence. This equivalence is a direct result of `gₓ` being -a non-degenerate bilinear form (O'Neill, Def 17(3), p. 46; Lemma 19, p. 47). -/ -def flatEquiv - (g : PseudoRiemannianMetric E H M n I) - (x : M) : - TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := - have : T2Space (TangentSpace I x) := inferInstanceAs (T2Space E) - LinearEquiv.toContinuousLinearEquiv - (LinearEquiv.ofBijective - ((g.flatL x).toLinearMap) - ⟨g.flatL_inj x, g.flatL_surj x⟩) - -lemma coe_flatEquiv - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (g.flatEquiv x : TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ)) = g.flatL x := rfl - -@[simp] -lemma flatEquiv_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - (g.flatEquiv x v) w = g.val x v w := rfl - -end Flat - -/-! ## Sharp -/ - -section Sharp - -/-- The "musical" isomorphism (index raising) from the dual of `TₓM` to `TₓM`. -This is the inverse of `flatEquiv g x`, and its existence as an isomorphism is -guaranteed by the non-degeneracy of `gₓ` (O'Neill, Lemma 19, p. 47). -/ -def sharpEquiv - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (TangentSpace I x →L[ℝ] ℝ) ≃L[ℝ] TangentSpace I x := - (g.flatEquiv x).symm - -/-- The index raising map `sharp` as a continuous linear map. -/ -def sharpL - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x := (g.sharpEquiv x).toContinuousLinearMap - -lemma sharpL_eq_toContinuousLinearMap - (g : PseudoRiemannianMetric E H M n I) (x : M) : - g.sharpL x = (g.sharpEquiv x).toContinuousLinearMap := rfl - -lemma coe_sharpEquiv - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (g.sharpEquiv x : (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x) = g.sharpL x := rfl - -/-- The index raising map `sharp` as a linear map. -/ -noncomputable def sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (TangentSpace I x →L[ℝ] ℝ) →ₗ[ℝ] TangentSpace I x := (g.sharpEquiv x).toLinearEquiv.toLinearMap - -@[simp] -lemma sharpL_apply_flatL - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : - g.sharpL x (g.flatL x v) = v := - (g.flatEquiv x).left_inv v - -@[simp] -lemma flatL_apply_sharpL - (g : PseudoRiemannianMetric E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : - g.flatL x (g.sharpL x ω) = ω := (g.flatEquiv x).right_inv ω - -/-- Applying `sharp` then `flat` recovers the original covector. -/ -@[simp] -lemma flat_sharp_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : - g.flat x (g.sharp x ω) = ω := - flatL_apply_sharpL g x ω - -@[simp] -lemma sharp_flat_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : - g.sharp x (g.flat x v) = v := - sharpL_apply_flatL g x v - -/-- The metric evaluated at `sharp ω₁` and `sharp ω₂`. -/ -@[simp] -lemma apply_sharp_sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - g.val x (g.sharpL x ω₁) (g.sharpL x ω₂) = ω₁ (g.sharpL x ω₂) := by - rw [← flatL_apply g x (g.sharpL x ω₁), flatL_apply_sharpL g x ω₁] - -/-- The metric evaluated at `v` and `sharp ω`. -/ -lemma apply_vec_sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) - (ω : TangentSpace I x →L[ℝ] ℝ) : - g.val x v (g.sharpL x ω) = ω v := by - rw [g.symm x v (g.sharpL x ω), ← flatL_apply g x (g.sharpL x ω), flatL_apply_sharpL g x ω] - -end Sharp - -/-! ## Cotangent -/ -section Cotangent - -variable {E : Type v} {H : Type w} {M : Type w} {n : WithTop ℕ∞} -variable [NormedAddCommGroup E] [NormedSpace ℝ E] -variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E] -variable {I : ModelWithCorners ℝ E H} -variable [IsManifold I (n + 1) M] -variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] - -/-- The value of the induced metric on the cotangent space at point `x`. -/ -noncomputable def cotangentMetricVal (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : ℝ := - g.val x (g.sharpL x ω₁) (g.sharpL x ω₂) - -@[simp] -lemma cotangentMetricVal_eq_apply_sharp (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentMetricVal g x ω₁ ω₂ = ω₁ (g.sharpL x ω₂) := - apply_sharp_sharp g x ω₁ ω₂ - -lemma cotangentMetricVal_symm (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentMetricVal g x ω₁ ω₂ = cotangentMetricVal g x ω₂ ω₁ := by - simpa only [cotangentMetricVal] using g.symm x (g.sharpL x ω₁) (g.sharpL x ω₂) - -/-- The induced metric on the cotangent space at point `x` as a bilinear form. -For covectors `ω₁` and `ω₂`, this gives `g(ω₁^#, ω₂^#)`, where `ω^#` is -the "sharp" musical isomorphism raising indices. -/ -noncomputable def cotangentToBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - LinearMap.BilinForm ℝ (TangentSpace I x →L[ℝ] ℝ) where - toFun ω₁ := { toFun := λ ω₂ => cotangentMetricVal g x ω₁ ω₂, - map_add' := λ ω₂ ω₃ => by - simp only [cotangentMetricVal, - ContinuousLinearMap.map_add], - map_smul' := λ c ω₂ => by - simp only [cotangentMetricVal, - map_smul, smul_eq_mul, RingHom.id_apply] } - map_add' := λ ω₁ ω₂ => by - ext ω₃ - simp only [cotangentMetricVal, - ContinuousLinearMap.map_add, - add_apply, - LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] - map_smul' := λ c ω₁ => by - ext ω₂ - simp only [cotangentMetricVal, - ContinuousLinearMap.map_smul, - _root_.smul_apply, - LinearMap.coe_mk, AddHom.coe_mk, - RingHom.id_apply, LinearMap.smul_apply] - -/-- The cometric on the cotangent space T_x*M at `x`, expressed as a quadratic form. -It is induced by the pseudo-Riemannian metric on the tangent space T_xM. -/ -noncomputable def cotangentToQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - QuadraticForm ℝ (TangentSpace I x →L[ℝ] ℝ) where - toFun ω := cotangentMetricVal g x ω ω - toFun_smul a ω := by - simp only [cotangentMetricVal, - ContinuousLinearMap.map_smul, - _root_.smul_apply, - smul_smul] - exists_companion' := - ⟨LinearMap.mk₂ ℝ (fun ω₁ ω₂ => - cotangentMetricVal g x ω₁ ω₂ + cotangentMetricVal g x ω₂ ω₁) - (fun ω₁ ω₂ ω₃ => by simp only [cotangentMetricVal, map_add, add_apply]; ring) - (fun a ω₁ ω₂ => by - simp only [cotangentMetricVal, map_smul, smul_apply]; ring) - (fun ω₁ ω₂ ω₃ => by - simp only [cotangentMetricVal, map_add, add_apply]; ring) - (fun a ω₁ ω₂ => by - simp only [cotangentMetricVal, map_smul, smul_apply]; ring), - by - intro ω₁ ω₂ - simp only [LinearMap.mk₂_apply, cotangentMetricVal] - simp only [ContinuousLinearMap.map_add, add_apply] - ring⟩ - -@[simp] -lemma cotangentToBilinForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentToBilinForm g x ω₁ ω₂ = cotangentMetricVal g x ω₁ ω₂ := rfl - -@[simp] -lemma cotangentToQuadraticForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω : TangentSpace I x →L[ℝ] ℝ) : - cotangentToQuadraticForm g x ω = cotangentMetricVal g x ω ω := rfl - -@[simp] -lemma cotangentToBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) : - (cotangentToBilinForm g x).IsSymm := ⟨cotangentMetricVal_symm g x⟩ - -/-- The cotangent metric is non-degenerate: if `cotangentMetricVal g x ω v = 0` for all `v`, - then `ω = 0`. -/ -lemma cotangentMetricVal_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω : TangentSpace I x →L[ℝ] ℝ) (h : ∀ v : TangentSpace I x →L[ℝ] ℝ, - cotangentMetricVal g x ω v = 0) : - ω = 0 := by - apply ContinuousLinearMap.ext - intro w - have hw := h (g.flatL x w) - rw [cotangentMetricVal_eq_apply_sharp, sharpL_apply_flatL] at hw - simpa using hw - -@[simp] -lemma cotangentToBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : - (cotangentToBilinForm g x).Nondegenerate := by - refine ⟨fun ω hω => cotangentMetricVal_nondegenerate g x ω hω, fun ω hω => ?_⟩ - refine cotangentMetricVal_nondegenerate g x ω fun v => ?_ - exact (cotangentMetricVal_symm g x ω v).trans (hω v) - -end Cotangent - -end PseudoRiemannianMetric -end -end PseudoRiemannianMetric diff --git a/Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean b/Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean deleted file mode 100644 index 17f7da09fe..0000000000 --- a/Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean +++ /dev/null @@ -1,224 +0,0 @@ -/- -Copyright (c) 2025 Matteo Cipollina. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Matteo Cipollina --/ -module - -public import Physlib.Mathematics.ForMathlib.Geometry.Metric.PseudoRiemannian.Defs -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 - -open Bundle Set Finset Function Filter Module Topology ContinuousLinearMap -open scoped Manifold Bundle LinearMap Dual -open PseudoRiemannianMetric InnerProductSpace - -noncomputable section - -variable {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] -variable {H : Type w} [TopologicalSpace H] -variable {M : Type w} [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E] -variable {I : ModelWithCorners ℝ E H} {n : ℕ∞} - -/-- A `RiemannianMetric` on a manifold `M` modeled on `H` with corners `I` (over the model space `E` -, typically `ℝ^m`) is a family of inner products on the tangent spaces `TangentSpace I x` -for each `x : M`. This family is required to vary smoothly with `x`, specifically with smoothness -`C^n`. - -This structure `extends` `PseudoRiemannianMetric`, inheriting the core properties of a -pseudo-Riemannian metric, such as being a symmetric, non-degenerate, `C^n`-smooth tensor field -of type `(0,2)`. The key distinguishing feature of a Riemannian metric is its positive-definiteness. - -The `pos_def'` field ensures that for any point `x` on the manifold and any non-zero tangent -vector `v` at `x`, the inner product `gₓ(v, v)` (denoted `val x v v`) is strictly positive. -This condition makes each `val x` (the metric at point `x`) a positive-definite symmetric -bilinear form, effectively an inner product, on the tangent space `TangentSpace I x`. - -Parameters: -- `I`: The `ModelWithCorners` for the manifold `M`. This defines the model space `E` (e.g., `ℝ^d`) - and the model space for the boundary `H`. -- `n`: The smoothness class of the metric, an `ℕ∞` value. The metric tensor components are `C^n` - functions. -- `M`: The type of the manifold. -- `[TopologicalSpace M]`: Assumes `M` has a topological structure. -- `[ChartedSpace H M]`: Assumes `M` is equipped with an atlas of charts to `H`. -- `[IsManifold I (n + 1) M]`: Assumes `M` is a manifold of smoothness `C^(n+1)`. - The manifold needs to be slightly smoother than the metric itself for certain constructions. -- `[inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)]`: - Ensures that each tangent space is a finite-dimensional real vector space. - -Fields: -- `toPseudoRiemannianMetric`: The underlying pseudo-Riemannian metric. This provides the - smooth family of symmetric bilinear forms `val : M → SymBilinForm ℝ (TangentSpace I ·)`. -- `pos_def'`: The positive-definiteness condition: `∀ x v, v ≠ 0 → val x v v > 0`. This asserts - that for any point `x` and any non-zero tangent vector `v` at `x`, the metric evaluated - on `(v, v)` is strictly positive. -/ -@[ext] -structure RiemannianMetric - (I : ModelWithCorners ℝ E H) (n : ℕ∞) (M : Type w) - [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (n + 1) M] - [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] - extends PseudoRiemannianMetric E H M n I where - /-- `gₓ(v, v) > 0` for all nonzero `v`. `val` is inherited from `PseudoRiemannianMetric`. -/ - pos_def' : ∀ x v, v ≠ 0 → val x v v > 0 -namespace RiemannianMetric - -variable {I : ModelWithCorners ℝ E H} {n : ℕ∞} {M : Type w} -variable [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (n + 1) M] -variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] - -/-- Coercion from RiemannianMetric to its underlying PseudoRiemannianMetric. -/ -instance : Coe (RiemannianMetric I n M) (PseudoRiemannianMetric E H M (n) I) where - coe g := g.toPseudoRiemannianMetric - -@[simp] -lemma pos_def (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) - (hv : v ≠ 0) : - (g.toPseudoRiemannianMetric.val x v) v > 0 := g.pos_def' x v hv - -/-- The quadratic form associated with a Riemannian metric is positive definite. -/ -@[simp] -lemma toQuadraticForm_posDef (g : RiemannianMetric I n M) (x : M) : - (g.toQuadraticForm x).PosDef := - λ v hv => g.pos_def x v hv - -lemma riemannian_metric_negDim_zero (g : RiemannianMetric I n M) (x : M) : - (g.toQuadraticForm x).negDim = 0 := by - apply QuadraticForm.rankNeg_eq_zero - exact g.toQuadraticForm_posDef x - -/-! ## InnerProductSpace structure from RiemannianMetric -/ - -section InnerProductSpace - -variable (g : RiemannianMetric I n M) (x : M) - -/-- The `InnerProductSpace.Core` structure for `TₓM` induced by a Riemannian metric `g`. - This provides the properties of an inner product: symmetry, - non-negativity, linearity, and definiteness. - Each `gₓ` is an inner product on `TₓM` (O'Neill, p. 55). -/ -@[reducible] -noncomputable def tangentInnerCore (g : RiemannianMetric I n M) (x : M) : - InnerProductSpace.Core ℝ (TangentSpace I x) where - inner := λ v w => g.inner x v w - conj_inner_symm := λ v w => by - simp only [inner_apply, conj_trivial] - exact g.toPseudoRiemannianMetric.symm x w v - re_inner_nonneg := λ v => by - simp only [inner_apply, RCLike.re_to_real] - by_cases hv : v = 0 - · simp [hv, map_zero] - · exact le_of_lt (g.pos_def x v hv) - add_left := λ u v w => by - simp only [inner_apply, map_add, add_apply] - smul_left := λ r u v => by - simp only [inner_apply, map_smul, conj_trivial] - rfl - definite := fun v (h_inner_zero : g.inner x v v = 0) => by - by_contra h_v_ne_zero - have h_pos : g.inner x v v > 0 := g.pos_def x v h_v_ne_zero - linarith [h_inner_zero, h_pos] - -/-! ### Local `NormedAddCommGroup` and `InnerProductSpace` Instances - -These instances are defined locally to be used when a specific Riemannian metric `g` -and point `x` are in context. They are not global instances to avoid typeclass conflicts -and to respect the fact that a manifold might not have a canonical Riemannian metric, -or might be studied with an indefinite (pseudo-Riemannian) metric where these -standard norm structures are not appropriate. -/ - -/-- Creates a `NormedAddCommGroup` structure on `TₓM` from a Riemannian metric `g`. -/ -@[reducible] -noncomputable def TangentSpace.metricNormedAddCommGroup (g : RiemannianMetric I n M) (x : M) : - NormedAddCommGroup (TangentSpace I x) := - @InnerProductSpace.Core.toNormedAddCommGroup ℝ (TangentSpace I x) _ _ _ (tangentInnerCore g x) - -/-- Creates an `InnerProductSpace` structure on `TₓM` from a Riemannian metric `g`. - Alternative implementation using `letI`. -/ -@[reducible] -noncomputable def TangentSpace.metricInnerProductSpace' (g : RiemannianMetric I n M) (x : M) : - letI := TangentSpace.metricNormedAddCommGroup g x - InnerProductSpace ℝ (TangentSpace I x) := - InnerProductSpace.ofCore (tangentInnerCore g x).toCore - -/-- Creates an `InnerProductSpace` structure on `TₓM` from a Riemannian metric `g`. -/ -@[reducible] -noncomputable def TangentSpace.metricInnerProductSpace (g : RiemannianMetric I n M) (x : M) : - let _ := TangentSpace.metricNormedAddCommGroup g x - InnerProductSpace ℝ (TangentSpace I x) := - let inner_core := tangentInnerCore g x - let _ := TangentSpace.metricNormedAddCommGroup g x - InnerProductSpace.ofCore inner_core.toCore - -/-- The norm on a tangent space induced by a Riemannian metric, defined as the square root - of the inner product of a vector with itself. -/ -noncomputable def norm (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - Real.sqrt (g.inner x v v) - --- Example using the norm function -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : - norm g x v ≥ 0 := Real.sqrt_nonneg _ - --- Example showing how to use the metric inner product space -example (g : RiemannianMetric I n M) (x : M) (v w : TangentSpace I x) : - (TangentSpace.metricInnerProductSpace g x).inner v w = g.inner x v w := by - let := TangentSpace.metricInnerProductSpace g x - rfl - -/-- Helper function to compute the norm on a tangent space from a Riemannian metric, - using the underlying `NormedAddCommGroup` structure. -/ -noncomputable def norm' (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - let normed_group := TangentSpace.metricNormedAddCommGroup g x - @Norm.norm (TangentSpace I x) (@NormedAddCommGroup.toNorm (TangentSpace I x) normed_group) v - --- Example: Using a custom norm function instead of the notation -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : - norm g x v ≥ 0 := by - unfold norm - apply Real.sqrt_nonneg - -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - letI := TangentSpace.metricNormedAddCommGroup g x - ‖v‖ - -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - let normed_group := TangentSpace.metricNormedAddCommGroup g x - @Norm.norm (TangentSpace I x) (@NormedAddCommGroup.toNorm (TangentSpace I x) normed_group) v - -lemma norm_eq_norm_of_metricNormedAddCommGroup (g : RiemannianMetric I n M) (x : M) - (v : TangentSpace I x) : norm g x v = @Norm.norm (TangentSpace I x) - (@NormedAddCommGroup.toNorm _ (TangentSpace.metricNormedAddCommGroup g x)) v := by - unfold norm - let normed_group := TangentSpace.metricNormedAddCommGroup g x - unfold TangentSpace.metricNormedAddCommGroup - simp only [inner_apply] - rfl - -end InnerProductSpace - -/-! ## Curve -/ - -section Curve - -/-- Calculates the length of a curve `γ` between parameters `t₀` and `t₁` -using the Riemannian metric `g`. This is defined as the integral of the norm of -the tangent vector along the curve. -/ -def curveLength (g : RiemannianMetric I n M) (γ : ℝ → M) (t₀ t₁ : ℝ) - {IDE : ModelWithCorners ℝ ℝ ℝ}[ChartedSpace ℝ ℝ] : ℝ := - ∫ t in t₀..t₁, norm g (γ t) ((mfderiv IDE I γ t) ((1 : ℝ) : TangentSpace IDE t)) - -end Curve - -end RiemannianMetric -end -end RiemannianMetric -end PseudoRiemannianMetric diff --git a/Physlib/Mathematics/ForMathlib/LinearMaps.lean b/Physlib/Mathematics/ForMathlib/LinearMaps.lean index 35fbdd5b8f..1a6593049a 100644 --- a/Physlib/Mathematics/ForMathlib/LinearMaps.lean +++ b/Physlib/Mathematics/ForMathlib/LinearMaps.lean @@ -7,7 +7,6 @@ module public import Mathlib.Algebra.Module.LinearMap.Defs public import Mathlib.Data.Fintype.BigOperators -public import Physlib.Meta.TODO.Basic public import Mathlib.Algebra.Ring.Rat /-! # Linear maps @@ -18,8 +17,6 @@ quadratic and cubic equations. -/ @[expose] public section -TODO "Replace the definitions of bi-linear maps in `./Mathematics/LinaerMaps` - with definitions from Mathlib." /-- The structure defining a homogeneous quadratic equation. -/ @[simp] diff --git a/Physlib/Mathematics/ForMathlib/PiTensorProduct.lean b/Physlib/Mathematics/ForMathlib/PiTensorProduct.lean deleted file mode 100644 index 045a5e8735..0000000000 --- a/Physlib/Mathematics/ForMathlib/PiTensorProduct.lean +++ /dev/null @@ -1,308 +0,0 @@ -/- -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 --/ -module - -public import Mathlib.LinearAlgebra.PiTensorProduct.Basic -/-! -# Pi Tensor Products - -The purpose of this file is to define some results about Pi tensor products not currently -in Mathlib. - -At some point these should either be up-streamed to Mathlib or replaced with definitions already -in Mathlib. - --/ - -@[expose] public section -namespace Physlib.PiTensorProduct - -noncomputable section tmulEquiv - -variable {R ι1 ι2 ι3 M N : Type} [CommSemiring R] - {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] - {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] - {s3 : ι3 → Type} [inst3 : (i : ι3) → AddCommMonoid (s3 i)] [inst3' : (i : ι3) → Module R (s3 i)] - [AddCommMonoid M] [Module R M] - [AddCommMonoid N] [Module R N] - -open TensorProduct - -/-! - -## induction principals for pi tensor products - --/ -attribute [local ext] TensorProduct.ext - -lemma induction_tmul {f g : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) →ₗ[R] M} - (h : ∀ p q, f (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q) - = g (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)) : f = g := by - ext - exact h _ _ - -lemma induction_assoc - {f g : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i) ⊗[R] (⨂[R] i : ι3, s3 i)) →ₗ[R] M} - (h : ∀ p q m, f (PiTensorProduct.tprod R p ⊗ₜ[R] - PiTensorProduct.tprod R q ⊗ₜ[R] PiTensorProduct.tprod R m) - = g (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q - ⊗ₜ[R] PiTensorProduct.tprod R m)) : f = g := by - ext - exact h _ _ _ - -lemma induction_assoc' - {f g : (((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) ⊗[R] (⨂[R] i : ι3, s3 i)) →ₗ[R] M} - (h : ∀ p q m, f ((PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q) ⊗ₜ[R] - PiTensorProduct.tprod R m) = g ((PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q) - ⊗ₜ[R] PiTensorProduct.tprod R m)) : f = g := by - ext - exact h _ _ _ - -lemma induction_tmul_mod - {f g : ((⨂[R] i : ι1, s1 i) ⊗[R] N) →ₗ[R] M} - (h : ∀ p m, f (PiTensorProduct.tprod R p ⊗ₜ[R] m) = g (PiTensorProduct.tprod R p ⊗ₜ[R] m)) : - f = g := by - ext - exact h _ _ - -lemma induction_mod_tmul - {f g : (N ⊗[R] (⨂[R] i : ι1, s1 i)) →ₗ[R] M} - (h : ∀ m p, f (m ⊗ₜ[R] PiTensorProduct.tprod R p) = g (m ⊗ₜ[R] PiTensorProduct.tprod R p)) : - f = g := by - ext - exact h _ _ - -/-! - -# Dependent type version of PiTensorProduct.tmulEquiv --/ - -/-- Given two maps `s1` and `s2` whose targets carry an instance of an additive commutative - monoid, the target of the sum of these two maps also carry an instance thereof. -/ -instance : (i : ι1 ⊕ ι2) → AddCommMonoid ((fun i => Sum.elim s1 s2 i) i) := fun i => - match i with - | Sum.inl i => inst1 i - | Sum.inr i => inst2 i - -/-- Given two maps `s1` and `s2` whose targets carry an instance of a module over `R`, - the target of the sum of these two maps also carry an instance thereof. -/ -instance : (i : ι1 ⊕ ι2) → Module R ((fun i => Sum.elim s1 s2 i) i) := fun i => - match i with - | Sum.inl i => inst1' i - | Sum.inr i => inst2' i - -/-- Takes a map `(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i` to the underlying map `(i : ι1) → s1 i `. -/ -def pureInl (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) : (i : ι1) → s1 i := - fun i => f (Sum.inl i) - -/-- Takes a map `(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i` to the underlying map `(i : ι2) → s2 i `. -/ -def pureInr (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) : (i : ι2) → s2 i := - fun i => f (Sum.inr i) - -section - -variable [DecidableEq (ι1 ⊕ ι2)] -omit inst1 inst2 - -set_option backward.isDefEq.respectTransparency false in -lemma pureInl_update_left [DecidableEq ι1] (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι1) - (v1 : s1 x) : pureInl (Function.update f (Sum.inl x) v1) = - Function.update (pureInl f) x v1 := by - funext y - simp only [pureInl, Function.update, Sum.inl.injEq, Sum.elim_inl] - split - · rename_i h - subst h - rfl - · rfl - -set_option backward.isDefEq.respectTransparency false in -lemma pureInr_update_left (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι1) - (v2 : s1 x) : - pureInr (Function.update f (Sum.inl x) v2) = (pureInr f) := by - funext y - simp [pureInr, Function.update] - -set_option backward.isDefEq.respectTransparency false in -lemma pureInr_update_right [DecidableEq ι2] (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι2) - (v2 : s2 x) : pureInr (Function.update f (Sum.inr x) v2) = - Function.update (pureInr f) x v2 := by - funext y - simp only [pureInr, Function.update, Sum.inr.injEq, Sum.elim_inr] - split - · rename_i h - subst h - rfl - · rfl - -set_option backward.isDefEq.respectTransparency false in -lemma pureInl_update_right (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι2) - (v1 : s2 x) : - pureInl (Function.update f (Sum.inr x) v1) = (pureInl f) := by - funext y - simp [pureInl, Function.update] - -end - -set_option backward.isDefEq.respectTransparency false in -/-- The multilinear map from `(Sum.elim s1 s2)` to `((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i)` - defined by splitting elements of `(Sum.elim s1 s2)` into two parts. -/ -def domCoprod : - MultilinearMap R (Sum.elim s1 s2) ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) where - toFun f := (PiTensorProduct.tprod R (pureInl f)) ⊗ₜ - (PiTensorProduct.tprod R (pureInr f)) - map_update_add' f xy v1 v2 := by - have : DecidableEq (ι1 ⊕ ι2) := inferInstance - have : DecidableEq ι1 := - @Function.Injective.decidableEq ι1 (ι1 ⊕ ι2) Sum.inl _ Sum.inl_injective - have : DecidableEq ι2 := - @Function.Injective.decidableEq ι2 (ι1 ⊕ ι2) Sum.inr _ Sum.inr_injective - match xy with - | Sum.inl xy => - simp only [Sum.elim_inl, pureInl_update_left, MultilinearMap.map_update_add, - pureInr_update_left, ← add_tmul] - | Sum.inr xy => - simp only [Sum.elim_inr, pureInl_update_right, pureInr_update_right, - MultilinearMap.map_update_add, ← tmul_add] - map_update_smul' f xy r p := by - have : DecidableEq (ι1 ⊕ ι2) := inferInstance - have : DecidableEq ι1 := - @Function.Injective.decidableEq ι1 (ι1 ⊕ ι2) Sum.inl _ Sum.inl_injective - have : DecidableEq ι2 := - @Function.Injective.decidableEq ι2 (ι1 ⊕ ι2) Sum.inr _ Sum.inr_injective - match xy with - | Sum.inl x => - simp only [Sum.elim_inl, pureInl_update_left, MultilinearMap.map_update_smul, - pureInr_update_left, smul_tmul, tmul_smul] - | Sum.inr y => - simp only [Sum.elim_inr, pureInl_update_right, pureInr_update_right, - MultilinearMap.map_update_smul, tmul_smul] - -/-- Expand `PiTensorProduct` on sums into a `TensorProduct` of two factors. -/ -def tmulSymm : (⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i) →ₗ[R] - ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) := PiTensorProduct.lift domCoprod - -/-- Produces a map `(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i` from a map `(i : ι1) → s1 i` and a - map `q : (i : ι2) → s2 i`. -/ -def elimPureTensor (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i := - fun x => - match x with - | Sum.inl x => p x - | Sum.inr x => q x - -section - -variable [DecidableEq ι1] [DecidableEq ι2] -omit inst1 inst2 - -set_option backward.isDefEq.respectTransparency false in -lemma elimPureTensor_update_right (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) - (y : ι2) (r : s2 y) : elimPureTensor p (Function.update q y r) = - Function.update (elimPureTensor p q) (Sum.inr y) r := by - funext x - match x with - | Sum.inl x => - rfl - | Sum.inr x => - change Function.update q y r x = _ - simp only [Function.update, Sum.inr.injEq, Sum.elim_inr] - split_ifs - · rename_i h - subst h - rfl - · rfl - -set_option backward.isDefEq.respectTransparency false in -@[simp] -lemma elimPureTensor_update_left (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) - (x : ι1) (r : s1 x) : elimPureTensor (Function.update p x r) q = - Function.update (elimPureTensor p q) (Sum.inl x) r := by - funext y - match y with - | Sum.inl y => - change (Function.update p x r) y = _ - simp only [Function.update, Sum.inl.injEq, Sum.elim_inl] - split_ifs - · rename_i h - subst h - rfl - · rfl - | Sum.inr y => - rfl - -end - -set_option backward.isDefEq.respectTransparency false in -/-- The multilinear map valued in multilinear maps defined by combining - `(i : ι1) → s1 i` and `q : (i : ι2) → s2 i` into a PiTensorProduct. -/ -def elimPureTensorMulLin : MultilinearMap R s1 - (MultilinearMap R s2 (⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i)) where - toFun p := { - toFun := fun q => PiTensorProduct.tprod R (elimPureTensor p q) - map_update_add' := fun m x v1 v2 => by - have : DecidableEq ι2 := inferInstance - have := Classical.decEq ι1 - simp only [elimPureTensor_update_right, MultilinearMap.map_update_add] - map_update_smul' := fun m x r v => by - have : DecidableEq ι2 := inferInstance - have := Classical.decEq ι1 - simp only [elimPureTensor_update_right, MultilinearMap.map_update_smul]} - map_update_add' p x v1 v2 := by - have : DecidableEq ι1 := inferInstance - have := Classical.decEq ι2 - apply MultilinearMap.ext - intro y - simp - map_update_smul' p x r v := by - have : DecidableEq ι1 := inferInstance - have := Classical.decEq ι2 - apply MultilinearMap.ext - intro y - simp - -/-- Collapse a `TensorProduct` of `PiTensorProduct` into a `PiTensorProduct`. -/ -def tmul : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) →ₗ[R] - ⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i := TensorProduct.lift { - toFun := fun a ↦ - PiTensorProduct.lift <| - PiTensorProduct.lift elimPureTensorMulLin a, - map_add' := fun a b ↦ by simp - map_smul' := fun r a ↦ by simp} - -/-- The equivalence formed by combining a `TensorProduct` into a `PiTensorProduct`. -/ -def tmulEquiv : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) ≃ₗ[R] - ⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i := - LinearEquiv.ofLinearMap tmul tmulSymm - (by - apply PiTensorProduct.ext - apply MultilinearMap.ext - intro p - simp only [tmul, tmulSymm, domCoprod, LinearMap.compMultilinearMap_apply, - LinearMap.coe_comp, Function.comp_apply, PiTensorProduct.lift.tprod, MultilinearMap.coe_mk, - lift.tmul, LinearMap.coe_mk, AddHom.coe_mk] - simp only [elimPureTensorMulLin, MultilinearMap.coe_mk, LinearMap.id_coe, id_eq] - apply congrArg - funext x - match x with - | Sum.inl x => rfl - | Sum.inr x => rfl) - (by - apply induction_tmul - intro p q - simp only [tmulSymm, domCoprod, tmul, elimPureTensorMulLin, LinearMap.coe_comp, - Function.comp_apply, lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod, - MultilinearMap.coe_mk, LinearMap.id_coe, id_eq] - rfl) - -@[simp] -lemma tmulEquiv_tmul_tprod (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) : - tmulEquiv ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) = - (PiTensorProduct.tprod R) (elimPureTensor p q) := by - simp only [tmulEquiv, tmul, elimPureTensorMulLin, LinearEquiv.coe_ofLinearMap, lift.tmul, - LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod, MultilinearMap.coe_mk] - -end tmulEquiv -end Physlib.PiTensorProduct diff --git a/Physlib/Mathematics/ForMathlib/Resolvent.lean b/Physlib/Mathematics/ForMathlib/Resolvent.lean deleted file mode 100644 index c831db20c6..0000000000 --- a/Physlib/Mathematics/ForMathlib/Resolvent.lean +++ /dev/null @@ -1,122 +0,0 @@ -/- -Copyright (c) 2026 Adam Bornemann. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Adam Bornemann --/ -module - -public import Mathlib.Analysis.Calculus.Deriv.Pow -public import Mathlib.Analysis.Distribution.TemperateGrowth -public import Mathlib.Analysis.Normed.Algebra.GelfandFormula -public import Mathlib.Analysis.Calculus.ContDiff.Operations -public import Mathlib.Analysis.Calculus.Deriv.Mul -public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs -/-! - -# Temperate growth of the resolvent of a non-real complex number - -## i. Overview - -For `z : ℂ` with `z.im ≠ 0`, every real number lies in the `ℝ`-resolvent set of `z`, so -Mathlib's algebra resolvent `resolvent (R := ℝ) z = fun t : ℝ ↦ Ring.inverse (↑t - z)` is a -globally defined, smooth map `ℝ → ℂ`. Its iterated derivatives have the closed form -`(-1)ⁿ · n! · (resolvent z)ⁿ⁺¹` and are globally bounded by `n! · (|z.im| ^ (n+1))⁻¹`; -consequently the resolvent has temperate growth. - -Smoothness and temperate growth are `fun_prop` lemmas, so composed variants such as the -affine reciprocal `t ↦ (z + a·t)⁻¹ = resolvent (-z) (a·t)` follow at call sites by -`fun_prop`. - -## ii. Key results - -- `mem_resolventSet_of_im_ne_zero` / `resolventSet_eq_univ` : every `t : ℝ` lies in - `resolventSet ℝ z` when `z.im ≠ 0`, i.e. `t - z` is invertible for all real `t`. -- `norm_resolvent_le` : the global bound `‖resolvent z t‖ ≤ |z.im|⁻¹`. -- `iteratedDeriv_resolvent` : the closed form - `iteratedDeriv n (resolvent z) = (-1)ⁿ · n! · (resolvent z)ⁿ⁺¹`. -- `norm_iteratedDeriv_resolvent_le` : the explicit derivative bounds - `‖iteratedDeriv n (resolvent z) t‖ ≤ n! · (|z.im| ^ (n+1))⁻¹`. -- `contDiff_resolvent`, `hasTemperateGrowth_resolvent` : smoothness and temperate growth - along `ℝ`, both tagged `@[fun_prop]`. - -## iii. Table of contents - -- A. The resolvent of a non-real complex number along `ℝ` - -## iv. References - -* None. --/ - -@[expose] public section - -open scoped ContDiff Nat - -namespace Physlib.Resolvent - -variable {z : ℂ} - -/-! -## A. The resolvent of a non-real complex number along `ℝ` --/ - -/-- Every real number lies in the `ℝ`-resolvent set of a non-real complex number: -`t - z` is invertible for all `t : ℝ`. -/ -lemma mem_resolventSet_of_im_ne_zero (hz : z.im ≠ 0) (t : ℝ) : t ∈ resolventSet ℝ z := by - rw [spectrum.mem_resolventSet_iff, isUnit_iff_ne_zero] - exact fun h ↦ hz (by simpa using congrArg Complex.im h) - -/-- The `ℝ`-resolvent set of a non-real complex number is all of `ℝ`. -/ -lemma resolventSet_eq_univ (hz : z.im ≠ 0) : resolventSet ℝ z = Set.univ := - Set.eq_univ_of_forall (mem_resolventSet_of_im_ne_zero hz) - -/-- The resolvent is globally bounded by `|z.im|⁻¹`: the imaginary part of the denominator -`t - z` is exactly `-z.im`. -/ -lemma norm_resolvent_le (hz : z.im ≠ 0) (t : ℝ) : ‖resolvent z t‖ ≤ |z.im|⁻¹ := by - rw [resolvent, Ring.inverse_eq_inv, norm_inv] - exact inv_anti₀ (abs_pos.mpr hz) (by simpa using Complex.abs_im_le_norm ((algebraMap ℝ ℂ) t - z)) - -/-- The resolvent of a non-real complex number is smooth along `ℝ`. -/ -@[fun_prop] -lemma contDiff_resolvent (hz : z.im ≠ 0) : ContDiff ℝ ∞ (resolvent (R := ℝ) z) := by - have : resolvent (R := ℝ) z = fun t : ℝ ↦ ((t : ℂ) - z)⁻¹ := funext fun t ↦ Ring.inverse_eq_inv _ - rw [this] - exact (Complex.ofRealCLM.contDiff.sub contDiff_const).inv fun t ↦ - (spectrum.mem_resolventSet_iff.mp (mem_resolventSet_of_im_ne_zero hz t)).ne_zero - -/-- Closed form for the iterated derivatives of the resolvent: the `n`-th derivative is -`(-1)ⁿ · n! · (resolvent z)ⁿ⁺¹`. -/ -lemma iteratedDeriv_resolvent (hz : z.im ≠ 0) (n : ℕ) : - iteratedDeriv n (resolvent (R := ℝ) z) - = fun t ↦ (-1) ^ n * (n ! : ℂ) * resolvent z t ^ (n + 1) := by - induction n with - | zero => simp - | succ n ih => - funext t - have hd := ((spectrum.hasDerivAt_resolvent_const_left - (mem_resolventSet_of_im_ne_zero hz t)).pow (n + 1)).const_mul ((-1) ^ n * (n ! : ℂ)) - simp only [Pi.pow_apply] at hd - rw [iteratedDeriv_succ, ih, hd.deriv] - push_cast [Nat.factorial_succ] - ring - -/-- Every iterated derivative of the resolvent is globally bounded, explicitly by -`n! · (|z.im| ^ (n + 1))⁻¹`. -/ -lemma norm_iteratedDeriv_resolvent_le (hz : z.im ≠ 0) (n : ℕ) (t : ℝ) : - ‖iteratedDeriv n (resolvent z) t‖ ≤ n ! * (|z.im| ^ (n + 1))⁻¹ := by - calc - _ = n ! * ‖resolvent z t‖ ^ (n + 1) := by simp [iteratedDeriv_resolvent, hz] - _ ≤ n ! * (|z.im| ^ (n + 1))⁻¹ := by - rw [← inv_pow] - gcongr - exact norm_resolvent_le hz t - -/-- The resolvent of a non-real complex number has temperate growth along `ℝ`. -/ -@[fun_prop] -lemma hasTemperateGrowth_resolvent (hz : z.im ≠ 0) : - Function.HasTemperateGrowth (resolvent (R := ℝ) z) := by - refine ⟨contDiff_resolvent hz, fun n ↦ ⟨0, n ! * (|z.im| ^ (n + 1))⁻¹, fun t ↦ ?_⟩⟩ - rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv, pow_zero, mul_one] - exact norm_iteratedDeriv_resolvent_le hz n t - -end Physlib.Resolvent diff --git a/Physlib/Meta/Linters/DefsWithUnderscore.lean b/Physlib/Meta/Linters/DefsWithUnderscore.lean index 228d233b68..a8f4ebc167 100644 --- a/Physlib/Meta/Linters/DefsWithUnderscore.lean +++ b/Physlib/Meta/Linters/DefsWithUnderscore.lean @@ -25,8 +25,7 @@ either generated by Lean or belongs to a declaration that is not user-facing: across projects, `_physlib` for a declaration in `Physlib` and so on. Mathlib exempts its own `_mathlib` suffix in the same way. * Anonymous instances that Lean disambiguates with a trailing number. Mathlib exempts `_1` and - `_2` but not `_3` and `_4`, which occur in - `Physlib.Mathematics.ForMathlib.DataStructures.FourTree.Basic`. + `_2` but not higher numbers such as `_3` and `_4`. `withDefsWithUnderscoreExemptions` wraps the linter so that these pass; every other declaration is reported as before. diff --git a/Physlib/QFT/AnomalyCancellation/Basic.lean b/Physlib/QFT/AnomalyCancellation/Basic.lean index 6a5e03ac0d..9446d5a15b 100644 --- a/Physlib/QFT/AnomalyCancellation/Basic.lean +++ b/Physlib/QFT/AnomalyCancellation/Basic.lean @@ -8,6 +8,7 @@ module public import Physlib.Mathematics.ForMathlib.LinearMaps public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.Tactic.Cases +public import Physlib.Meta.TODO.Basic /-! # Anomaly cancellation conditions @@ -567,3 +568,6 @@ TODO "Anomaly cancellation conditions can be derived formally from the gauge gro TODO "Anomaly cancellation conditions can be defined using algebraic varieties. Link such an approach to the approach here." + +TODO "Replace the definitions of bi-linear maps in + `Physlib.Mathematics.ForMathlib.LinearMaps` with definitions from Mathlib." diff --git a/scripts/MetaPrograms/module_doc_no_lint.txt b/scripts/MetaPrograms/module_doc_no_lint.txt index a7d316e859..f5d64c0945 100644 --- a/scripts/MetaPrograms/module_doc_no_lint.txt +++ b/scripts/MetaPrograms/module_doc_no_lint.txt @@ -30,19 +30,14 @@ Physlib/Mathematics/Distribution/Function/InvPowMeasure.lean Physlib/Mathematics/Distribution/Function/IsDistBounded.lean Physlib/Mathematics/Distribution/Function/OfFunction.lean Physlib/Mathematics/Distribution/PowMul.lean -Physlib/Mathematics/ForMathlib/DataStructures/FourTree/Basic.lean -Physlib/Mathematics/ForMathlib/DataStructures/FourTree/UniqueMap.lean Physlib/Mathematics/ForMathlib/DataStructures/Matrix/LieTrace.lean Physlib/Mathematics/ForMathlib/FDerivCurry.lean Physlib/Mathematics/ForMathlib/Fin.lean Physlib/Mathematics/ForMathlib/Fin/Involutions.lean -Physlib/Mathematics/ForMathlib/Geometry/Metric/PseudoRiemannian/Defs.lean -Physlib/Mathematics/ForMathlib/Geometry/Metric/Riemannian/Defs.lean Physlib/Mathematics/ForMathlib/LinearMaps.lean Physlib/Mathematics/ForMathlib/List.lean Physlib/Mathematics/ForMathlib/List/InsertIdx.lean Physlib/Mathematics/ForMathlib/List/InsertionSort.lean -Physlib/Mathematics/ForMathlib/PiTensorProduct.lean Physlib/Mathematics/ForMathlib/SchurTriangulation.lean Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean Physlib/Mathematics/Groups/SO3/Basic.lean From 440a5a00d204f942a114d6cec135bfbac40be932 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:44:27 +0100 Subject: [PATCH 6/7] feat: Add to CI --- .github/workflows/build.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 7a6ec517a5..af42b2b30e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -112,6 +112,11 @@ jobs: if: ${{ !cancelled() && steps.alpha_build.outcome == 'success' }} run: env LEAN_ABORT_ON_PANIC=1 lake exe alphaFileImports + # Only reads import headers, so it does not depend on any build having succeeded. + - name: Check ForMathlib imports and uses + if: ${{ !cancelled() }} + run: env LEAN_ABORT_ON_PANIC=1 lake exe forMathlib_lint + # Runs the occasionally used scripts (TODO_to_yml, stats, informal, make_tag), which # import Physlib, QuantumInfo and PhyslibAlpha, so both builds must have succeeded. - name: auxiliary script test From 97e587dc5a4465f173ce10c88e00366dd73d736e Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:46:37 +0100 Subject: [PATCH 7/7] Update AGENTS.md --- AGENTS.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/AGENTS.md b/AGENTS.md index 8fbffc9e9c..6bf4d25d86 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -55,6 +55,8 @@ When a long proof cannot be split, make sure it contains comments. - New physics terms that trip the spell-checker go in `scripts/MetaPrograms/spellingWords.txt`. - Check that `lake build` works (run `lake exe cache get` first). - Check that `lake exe lint_all` passes. +- Check that `lake exe forMathlib_lint` passes: files in `Physlib/Mathematics/ForMathlib/` may only + import from within that directory, and each must be used outside it. - Check `./scripts/lint-style.sh`, but **commit your changes first**; this linter reads committed state. - Check that `lake exe auxillary_script_test` passes (needs `Physlib`, `QuantumInfo` and `PhyslibAlpha` built).