feat: notation for Euclidean space

[eric-wieser]

This adds !ₑ[1, 2, 3] notation for (WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3], which is a term of type EuclideanSpace 𝕜 (Fin 3).

This reduces the temptation to write the type-incorrect ![1, 2, 3] that has the wrong norm.

Notation Zulip poll.

---

We could consider introducing this more generally for other Lp-norms; notation suggestions welcome. This might be an argument for using !₂[1, 2, 3] instead of !ₑ[1, 2, 3]

[github-actions[bot]]

PR summary 83e83066c0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.InnerProductSpace.PiL2	1803	1804	+1 (+0.06%)
Mathlib.Analysis.Quaternion	1805	1806	+1 (+0.06%)

Import changes for all files

Files

Import difference

270 files Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.NumberTheory.GaussSum Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Complex Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Probability.Kernel.Composition Mathlib.Analysis.RCLike.Inner Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Probability.Kernel.IntegralCompProd Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.InnerProductSpace.Positive Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Topology.CWComplex Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Combinatorics.Additive.Randomisation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.Fermat Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.Quaternion Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.MeasureTheory.Function.Jacobian Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.Convex.Measure Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.ConstantSpeed Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Probability.Kernel.MeasureCompProd Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Analysis.Matrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.Convolution Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.Analysis.MellinInversion Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.NumberTheory.WellApproximable Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Distributions.Pareto Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Probability.Kernel.Condexp Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Geometry.Euclidean.Triangle Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Density Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Geometry.Manifold.Instances.Sphere

1

---

Declarations diff

+ EuclideanSpace.delabVecNotation

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

@digama0, any idea what's up with uncaught exception: parser 'subscript' was not found in the CI logs for lake exe check-yaml?

[digama0]

My guess is that one of the linters is elaborating something in an empty environment, and it's failing to interpret the syntax objects. See 6ed0fa63 which was about a similar issue.

[eric-wieser]

Here there's no panic to speak of, and the issue seems to be just a regular IO exception being thrown.

I don't think linters are to blame, since adding

Lean.Elab.Command.lintersRef.set #[]

to the start of main doesn't help.

[eric-wieser]

@digama0, I think these lines are somehow not running:

https://github.com/leanprover-community/mathlib4/blob/85ec5bfdc334783e7cc63ce1f1a3679eaacba054/Mathlib/Util/Superscript.lean#L279-L285

[mathlib-bors[bot]]

:v: eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style