[Merged by Bors] - chore: avoid importing ContDiff.Defs in FDeriv.Analytic
#19374
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
22 tasks
PR summary 0218af6767
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.Calculus.FDeriv.Analytic | 1516 | 1515 | -1 (-0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
38 filesMathlib.Analysis.Calculus.Deriv.Inv Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Combinatorics.Derangements.Exponential Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Probability.Distributions.Poisson Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Calculus.LogDeriv Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Series |
-1 |
154 filesMathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.Complex.Angle Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Tactic.FunProp.ContDiff Mathlib.NumberTheory.GaussSum Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Geometry.Manifold.Complex Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.NumberTheory.LSeries.Deriv Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.Inversion Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.NumberTheory.NumberField.Completion Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Probability.Distributions.Gaussian Mathlib.Geometry.Manifold.BumpFunction Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.Data.Real.Pi.Leibniz Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.Fermat Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Data.Real.Pi.Bounds Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ODE.Gronwall Mathlib.RingTheory.Polynomial.Selmer Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.Tactic.FunProp.Differentiable Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.MellinInversion Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Data.Complex.ExponentialBounds Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.Geometry.Manifold.Instances.Sphere |
1 |
20 filesMathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.HurwitzZeta |
2 |
Mathlib.Analysis.Calculus.ContDiff.Analytic (new file) Mathlib.Analysis.Calculus.ContDiff.CPolynomial (new file) |
1517 |
Declarations diff
+ AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
leanprover-community-bot-assistant
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 27, 2024
For this, move the results needing `ContDiff` to two new files. The reason of this change is that I will import `FDeriv.Analytic` in `ContDiff.Defs` in #17152
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
ContDiff.Defs in FDeriv.AnalyticContDiff.Defs in FDeriv.Analytic
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
For this, move the results needing
ContDiffto two new files. The reason of this change is that I will importFDeriv.AnalyticinContDiff.Defsin #17152