[Merged by Bors] - refactor: allow deriv to be used on topological vector spaces
#19108
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
This lets us hide the implementation details, and replace them with `IsLittleOTVS` later.
Notably, this allows us to _state_ results about derivatives of matrices, without the statement encoding a choice of norm. For now, it is not possible to prove any of these statements without locally constructing a norm.
PR summary a9c2ed2883
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.Calculus.FDeriv.Basic | 1435 | 1438 | +3 (+0.21%) |
| Mathlib.Analysis.Calculus.Deriv.Basic | 1440 | 1443 | +3 (+0.21%) |
| Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries | 1509 | 1512 | +3 (+0.20%) |
| Mathlib.Analysis.Calculus.FDeriv.Mul | 1536 | 1539 | +3 (+0.20%) |
| Mathlib.Analysis.Calculus.FDeriv.WithLp | 1648 | 1651 | +3 (+0.18%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv | 1783 | 1786 | +3 (+0.17%) |
| Mathlib.Analysis.InnerProductSpace.Calculus | 1825 | 1828 | +3 (+0.16%) |
| Mathlib.Analysis.SpecialFunctions.Pow.Deriv | 1837 | 1840 | +3 (+0.16%) |
| Mathlib.Analysis.Fourier.FourierTransformDeriv | 2125 | 2128 | +3 (+0.14%) |
| Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable | 2190 | 2193 | +3 (+0.14%) |
Import changes for all files
| Files | Import difference |
|---|---|
77 filesMathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Analysis.Fourier.ZMod Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.UpperHalfPlane.Manifold 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.LSeries.Dirichlet Mathlib.NumberTheory.Fermat Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Analysis.Normed.Algebra.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Polynomial.Selmer Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Tactic Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.ModularForms.QExpansion |
2 |
262 filesMathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.Analysis.Complex.Angle Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Tactic.FunProp.ContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Complex.AbsMax Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.Instances.Real Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Geometry.Manifold.Complex Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Complex.Periodic Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Analysis.Complex.TaylorSeries Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.NumberTheory.LSeries.Deriv Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Probability.Distributions.Gaussian Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Probability.Distributions.Poisson Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Analysis.Calculus.Darboux Mathlib.MeasureTheory.Function.Jacobian Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Data.Real.Pi.Bounds Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.Implicit Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Tactic.FunProp.Differentiable Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Analysis.Convolution Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.MellinInversion Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Analysis.BoundedVariation Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Geometry.Manifold.Metrizable Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Data.Real.Pi.Wallis Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product |
3 |
Declarations diff
+ HasFDerivAtFilter.isLittleO
+ HasFDerivAtFilter.of_isLittleO
+ HasStrictFDerivAt.isLittleO
+ HasStrictFDerivAt.of_isLittleO
+ hasFDerivAtFilter_iff_isLittleO
+ hasStrictFDerivAt_iff_isLittleO
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).
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
leanprover-community-bot-assistant
added
the
merge-conflict
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
leanprover-community-bot-assistant
removed
the
merge-conflict
This reverts commit 903342c.
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
|
!bench |
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
1 task
|
@eric-wieser Do you know why it makes everything slower? |
|
@urkud: I have a good idea; we have hundreds of statements about
This also is probably the cause of the various unification woes, in that in many case the correct instances can no longer be found by unification alone. It's also possible that the fixes that were needed to make unification succeed at all in some places would be effective at making it faster in others; but without per-lemma benchmarking, it would be unreasonably hard to track those down. Largely I think the performance cost is worth it here. |
leanprover-community-bot-assistant
added
the
merge-conflict
eric-wieser
removed
the
merge-conflict
|
!bench |
This comment was marked as outdated.
This comment was marked as outdated.
|
Some more precise profiles from
Unfortunately without leanprover/lean4#6363 the tools to compare these crash, but a comparison between windows suggests that |
|
!bench |
|
Here are the benchmark results for commit a9c2ed2. Benchmark Metric Change
=========================================================================
- ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions 4.0%
- ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions 6.6%
- ~Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries instructions 13.0%
- ~Mathlib.Analysis.Calculus.Deriv.Basic instructions 38.7%
- ~Mathlib.Analysis.Calculus.Deriv.Comp instructions 46.1%
- ~Mathlib.Analysis.Calculus.Deriv.Mul instructions 28.5%
- ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions 12.3%
- ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions 11.5%
- ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions 17.5%
- ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions 11.9%
- ~Mathlib.Analysis.Calculus.MeanValue instructions 17.0%
- ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions 11.8%
- ~Mathlib.Geometry.Manifold.MFDeriv.NormedSpace instructions 4.0%
- ~Mathlib.MeasureTheory.Integral.FundThmCalculus instructions 15.4% |
|
These slowdowns might be large percentage-wise but these files are really quick to build. bors merge |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 24, 2024
Notably, this allows us to _state_ results about derivatives of matrices, without the statement encoding a choice of norm. For now, it is not possible to prove any of these statements without locally constructing a norm. This generalizes: * `HasFDerivAtFilter` * `HasFDerivWithinAt` * `HasFDerivAt` * `HasStrictFDerivAt` * `DifferentiableWithinAt` * `DifferentiableAt` * `fderivWithin` * `fderiv` * `DifferentiableOn` * `Differentiable` * `HasDerivAtFilter` * `HasDerivWithinAt` * `HasDerivAt` * `HasStrictDerivAt` * `derivWithin` * `deriv` Continues from [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/generalizing.20deriv.20to.20TVS/near/482705911).
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
deriv to be used on topological vector spacesderiv to be used on topological vector spaces
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.
Notably, this allows us to state results about derivatives of matrices, without the statement encoding a choice of norm.
For now, it is not possible to prove any of these statements without locally constructing a norm.
This generalizes:
HasFDerivAtFilterHasFDerivWithinAtHasFDerivAtHasStrictFDerivAtDifferentiableWithinAtDifferentiableAtfderivWithinfderivDifferentiableOnDifferentiableHasDerivAtFilterHasDerivWithinAtHasDerivAtHasStrictDerivAtderivWithinderivContinues from this Zulip thread.
HasStrictFDerivAta structure #19104IsLittleOTVS#9675