[Merged by Bors] - feat: if a function is analytic on a set, its derivative also is, even if the space is not complete #17221
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
PR summary 588d6a43ef
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.Calculus.FDeriv.Analytic | 1394 | 1402 | +8 (+0.57%) |
Import changes for all files
| Files | Import difference |
|---|---|
161 filesMathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Complex Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.NumberTheory.NumberField.Discriminant Mathlib.NumberTheory.NumberField.EquivReindex 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.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.NumberTheory.LSeries.Deriv Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow 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.Analysis.Complex.CauchyIntegral Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.Data.Real.Pi.Leibniz Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.NumberTheory.Liouville.Measure Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.Analytic.Meromorphic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic 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.Analysis.InnerProductSpace.EuclideanDist Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup 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.RingTheory.Polynomial.Selmer Mathlib.Geometry.Manifold.IntegralCurve Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.NumberTheory.ZetaValues Mathlib.LinearAlgebra.Matrix.LDL 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.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.Distribution.SchwartzSpace 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.Geometry.Manifold.Instances.Sphere |
1 |
Mathlib.Analysis.Normed.Algebra.QuaternionExponential |
2 |
97 filesMathlib.NumberTheory.Liouville.LiouvilleWith Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Tactic.FunProp.ContDiff Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.NumberTheory.Liouville.LiouvilleNumber Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.LHopital Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.Darboux Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.NumberTheory.Liouville.Basic Mathlib.Data.Real.Pi.Bounds Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.NumberTheory.ModularForms.Basic Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Tactic.FunProp.Differentiable Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.NumberTheory.Liouville.Residual Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Calculus.Dslope Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.NumberTheory.Bertrand Mathlib.Geometry.Manifold.Metrizable Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Data.Complex.ExponentialBounds Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product |
7 |
5 filesMathlib.Combinatorics.Derangements.Exponential Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Probability.Distributions.Poisson Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.Trigonometric.Series |
8 |
Declarations diff
+ AnalyticAt.fderiv
+ AnalyticOn.exists_hasFTaylorSeriesUpToOn
+ AnalyticOn.fderivWithin
+ AnalyticOn.hasFTaylorSeriesUpToOn
+ AnalyticOn.iteratedFDerivWithin
+ AnalyticOnNhd.deriv_of_isOpen
+ AnalyticOnNhd.fderiv_of_isOpen
+ AnalyticOnNhd.hasFTaylorSeriesUpToOn
+ AnalyticOnNhd.iteratedFDeriv_of_isOpen
+ AnalyticWithinAt.differentiableWithinAt
+ AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn
+ HasFPowerSeriesWithinAt.differentiableWithinAt
+ HasFPowerSeriesWithinAt.fderivWithin_eq
+ HasFPowerSeriesWithinAt.hasFDerivWithinAt
+ HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt
+ HasFPowerSeriesWithinOnBall.differentiableOn
+ HasFPowerSeriesWithinOnBall.fderivWithin
+ HasFPowerSeriesWithinOnBall.fderivWithin_eq
+ HasFPowerSeriesWithinOnBall.hasFDerivWithinAt
+ HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
+ PartialHomeomorph.analyticAt_symm
+ PartialHomeomorph.analyticAt_symm'
+ _root_.HasFDerivAt.linear_multilinear_comp
+ _root_.HasFDerivAt.multilinear_comp
+ _root_.HasFDerivWithinAt.linear_multilinear_comp
+ _root_.HasFDerivWithinAt.multilinear_comp
+ embedding
+ hasFDerivAt_uncurry_of_multilinear
+ postcomp
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.
22 tasks
leanprover-community-bot-assistant
added
the
merge-conflict
urkud
reviewed
Sep 29, 2024
urkud
reviewed
Sep 29, 2024
leanprover-community-bot-assistant
removed
the
merge-conflict
|
Thanks! 🎉 |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 4, 2024
…n if the space is not complete (#17221) We already have a version of this theorem, but assuming completeness while this is not necessary: if the function is differentiable, then the power series for its derivative converges, to the given differential (since this is the case in the completion, and the embedding in the completion is an embedding). This result requires expanding the API around derivatives of analytic functions. As a byproduct, we also write down the derivative of linear maps into multilinear maps (which will be needed for the Faa di Bruno formula).
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
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.
We already have a version of this theorem, but assuming completeness while this is not necessary: if the function is differentiable, then the power series for its derivative converges, to the given differential (since this is the case in the completion, and the embedding in the completion is an embedding).
This result requires expanding the API around derivatives of analytic functions. As a byproduct, we also write down the derivative of linear maps into multilinear maps (which will be needed for the Faa di Bruno formula).