refactor(Analysis): golf 100 files

[yuanyi-350]

This PR is an experimental project. In this PR, we use an Agent to automatically scan and attempt to simplify proofs. We hope to eventually effectively golf 100 files and avoid reinventing the wheel in mathlib.

We have chosen Mathlib/Analysis as the testing ground. If this experiment is very successful and accepted by the mathlib community, we would be honored to open source it.

The relevant projects includes

• refactor(MeasureTheory): golf 100 files #38104, which golfs Mathlib/MeasureTheory.
• refactor(NumberTheory): Golf 100 files #38144, which golfs Mathlib/NumberTheory.

This PR serves as an index. For the actual code review, please refer to the individual PRs linked below. Each of those PRs modifies only a single file to facilitate the review process.

• depends on: refactor(Analysis): golf Mathlib/Analysis/Normed/Operator/Mul #38272
• depends on: [Merged by Bors] - feat(MeasureTheory/Integral/IntervalIntegral): weaken assumptions in trapezoidal_error_le #37555
• depends on: [Merged by Bors] - chore(Probability): shorten proof of condExp_indep_eq #37731
• depends on: [Merged by Bors] - chore(NumberTheory/FermatPsp): weaken assumptions in psp_from_prime_gt_p #37737
• depends on: [Merged by Bors] - chore(Analysis, MeasureTheory): golf MeanInequalities and LiminfLimsup proofs #37754
• depends on: [Merged by Bors] - chore: golf proofs in FDeriv/Symmetric #37785
• depends on: [Merged by Bors] - refactor: simplify isLocalRing_of_isAdicComplete_maximal #37788
• depends on: [Merged by Bors] - chore: golf proofs in Mathlib/RingTheory/PowerSeries/Substitution.lean #37821
• depends on: [Merged by Bors] - chore: golf some calculus proofs #37876
• depends on: [Merged by Bors] - chore(Analysis/Convex/Approximation): reuse sSup_of_nat_affine_eq #37981
• depends on: [Merged by Bors] - chore(Analysis): golf files in Mathlib/Analysis/CStarAlgebra #37987
• depends on: [Merged by Bors] - chore(Mathlib/Analysis/CStarAlgebra/Projection.lean): golf lemma #37989
• depends on: [Merged by Bors] - chore(Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean): automated extraction #37991
• depends on: [Merged by Bors] - chore(Analysis): golf Basic, Exponential, and ContinuousFunctionalCalculus/Unique #38006
• depends on: [Merged by Bors] - chore(Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean): automated extraction #38010
• depends on: refactor(Analysis): golf Mathlib/Analysis/SpecialFunctions/Gamma/Basic #38273
• depends on: refactor(Analysis): golf Mathlib/Analysis/Complex/Trigonometric #38274

---

[github-actions]

PR summary c3e588b468

Import changes exceeding 2%

%	File
+2.38%	Mathlib.Analysis.Complex.OperatorNorm
+17.75%	Mathlib.Analysis.PSeries

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.PSeries	1780	2096	+316 (+17.75%)
Mathlib.Analysis.Complex.OperatorNorm	2018	2066	+48 (+2.38%)
Mathlib.Analysis.Normed.Ring.Lemmas	1387	1390	+3 (+0.22%)
Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation	2687	2691	+4 (+0.15%)
Mathlib.Analysis.Complex.CauchyIntegral	2490	2493	+3 (+0.12%)
Mathlib.Analysis.Complex.Hadamard	2514	2517	+3 (+0.12%)
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform	2556	2559	+3 (+0.12%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation	2752	2755	+3 (+0.11%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order	2756	2759	+3 (+0.11%)

Import changes for all files

Files	Import difference
10 files Mathlib.Algebra.Module.ZLattice.Summable Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.ZetaValues	1
3 files Mathlib.Analysis.Normed.Field.Instances Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.ContinuousMap.Polynomial	2
180 files Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.Fuglede Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.BorelCaratheodory Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.Liouville Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.Harmonic.Poisson Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Poisson Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.GaussLucas Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Measure Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.Sobolev Mathlib.Analysis.Distribution.Support Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions Mathlib.Analysis.InnerProductSpace.StandardSubspace Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.MellinInversion Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.Normed.Algebra.GelfandMazur Mathlib.Analysis.Normed.Ring.InfiniteSum Mathlib.Analysis.Normed.Ring.Int Mathlib.Analysis.Normed.Ring.Lemmas Mathlib.Analysis.Polynomial.Factorization Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Geometry.Manifold.Complex Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.NumberTheory.ArithmeticFunction.Carmichael Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Completion.InfinitePlace Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances Mathlib.NumberTheory.NumberField.Completion.Ramification Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Completion Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.ZMod.UnitsCyclic Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.MetricSpace.ThickenedIndicator	3
7 files Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable	4
Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence	38
Mathlib.Analysis.Complex.OperatorNorm	48
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable	78
Mathlib.NumberTheory.SumPrimeReciprocals	313
Mathlib.Analysis.PSeries	316

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (0.99, 0.07)

Current number	Change	Type
14	1	backward.inferInstanceAs.wrap.data
6531	-3	backward.isDefEq.respectTransparency

Current commit be67e5fee6
Reference commit c3e588b468

You can run this locally as

./scripts/reporting/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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[themathqueen]

I know this is marked WIP, but I just want to say that you should split this into multiple PRs when you're ready. Other golfing PRs usually golf about 5-10 results per PR (I think), so maybe aim for that?

[yuanyi-350]

I know this is marked WIP, but I just want to say that you should split this into multiple PRs when you're ready. Other golfing PRs usually golf about 5-10 results per PR (I think), so maybe aim for that?

@themathqueen , Thank you for your suggestion. We will split this into many PRs for easier maintenance. The purpose of this PR is to serve as a catalog and to demonstrate the golfing potential of mathlib4.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[euprunin]

This PR is an experimental project. In this PR, we use an Agent to automatically scan and attempt to simplify proofs. We hope to eventually effectively golf 100 files and avoid reinventing the wheel in mathlib.

We have chosen Mathlib/Analysis as the testing ground. There are currently 785 files in total, and we have scanned 122 so far.

If this experiment is very successful and accepted by the mathlib community, we would be honored to open source it.

Thanks for running this golfing experiment!

Have you made any progress on open-sourcing the code behind it? Is it available somewhere? I'd be very curious to take a look.

[mathlib-dependent-issues]

This PR/issue depends on:

• refactor(Analysis): golf Mathlib/Analysis/Normed/Operator/Mul #38272
• [Merged by Bors] - feat(MeasureTheory/Integral/IntervalIntegral): weaken assumptions in trapezoidal_error_le #37555
• [Merged by Bors] - chore(Probability): shorten proof of condExp_indep_eq #37731
• [Merged by Bors] - chore(NumberTheory/FermatPsp): weaken assumptions in psp_from_prime_gt_p #37737
• [Merged by Bors] - chore(Analysis, MeasureTheory): golf MeanInequalities and LiminfLimsup proofs #37754
• [Merged by Bors] - chore: golf proofs in FDeriv/Symmetric #37785
• [Merged by Bors] - refactor: simplify isLocalRing_of_isAdicComplete_maximal #37788
• [Merged by Bors] - chore: golf proofs in Mathlib/RingTheory/PowerSeries/Substitution.lean #37821
• [Merged by Bors] - chore: golf some calculus proofs #37876
• [Merged by Bors] - chore(Analysis/Convex/Approximation): reuse sSup_of_nat_affine_eq #37981
• [Merged by Bors] - chore(Analysis): golf files in Mathlib/Analysis/CStarAlgebra #37987
• [Merged by Bors] - chore(Mathlib/Analysis/CStarAlgebra/Projection.lean): golf lemma #37989
• [Merged by Bors] - chore(Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean): automated extraction #37991
• [Merged by Bors] - chore(Analysis): golf Basic, Exponential, and ContinuousFunctionalCalculus/Unique #38006
• [Merged by Bors] - chore(Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean): automated extraction #38010
• refactor(Analysis): golf Mathlib/Analysis/SpecialFunctions/Gamma/Basic #38273
• refactor(Analysis): golf Mathlib/Analysis/Complex/Trigonometric #38274
  By Dependent Issues (🤖). Happy coding!