[Merged by Bors] - chore(Analysis/Analytic): split `Analytic.Basic` by vasnesterov · Pull Request #26270 · leanprover-community/mathlib4

vasnesterov · 2025-06-22T13:53:36Z

Move the results on the radius of convergence from Analytic/Basic.lean to a new file Analytic/ConvergenceRadius.lean.

depends on: [Merged by Bors] - feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap #26255

…ries_apply_nonzero

github-actions · 2025-06-22T13:54:47Z

PR summary 0eeb5f2502

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Analytic.OfScalars	1679	1678	-1 (-0.06%)

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Analytic.OfScalars` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric`	-1
398 files `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomialDef` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.Analysis.Analytic.IteratedFDeriv` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.Analytic.Order` `Mathlib.Analysis.Analytic.Polynomial` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.ContDiff.Operations` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.RestrictScalars` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.Deriv.CompMul` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.MeanValue` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Analysis.Calculus.Deriv.Shift` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.Analysis.Calculus.DerivativeTest` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.FDeriv.Pow` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction` `Mathlib.Analysis.Complex.ValueDistribution.CountingFunction` `Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem` `Mathlib.Analysis.Complex.ValueDistribution.ProximityFunction` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.Harmonic.Basic` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.Laplacian` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.InnerProductSpace.Trace` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Divisor` `Mathlib.Analysis.Meromorphic.FactorizedRational` `Mathlib.Analysis.Meromorphic.Gamma` `Mathlib.Analysis.Meromorphic.IsolatedZeros` `Mathlib.Analysis.Meromorphic.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Meromorphic.TrailingCoefficient` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.NormedSpace.DualNumber` `Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrability.Basic` `Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic` `Mathlib.Analysis.SpecialFunctions.Integrals.Basic` `Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.Pochhammer` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.Computability.AkraBazzi.SumTransform` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Deprecated.AnalyticManifold` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.AnalyticManifold` `Mathlib.Geometry.Manifold.Bordism` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Geometry.Manifold.ContMDiff.Constructions` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.GroupLieAlgebra` `Mathlib.Geometry.Manifold.Instances.Icc` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.IsManifold.ExtChartAt` `Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Riemannian.Basic` `Mathlib.Geometry.Manifold.Riemannian.PathELength` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.Riemannian` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorField.LieBracket` `Mathlib.Geometry.Manifold.VectorField.Pullback` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.InformationTheory.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc` `Mathlib.MeasureTheory.Integral.CircleAverage` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntegrationByParts` `Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff` `Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.CharacteristicFunction` `Mathlib.MeasureTheory.Measure.FiniteMeasureExt` `Mathlib.MeasureTheory.Measure.IntegralCharFun` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.NumberTheory.ModularForms.LevelOne` `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` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Embeddings` `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.Ideal` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `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.NumberTheory.Transcendental.Lindemann.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian.Basic` `Mathlib.Probability.Distributions.Gaussian.Real` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Probability.Moments.ComplexMGF` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Moments.SubGaussian` `Mathlib.Probability.Moments.Tilted` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Compactification.OnePoint.Sphere` `Mathlib.Topology.MetricSpace.HausdorffDimension`	1
`Mathlib.Analysis.Analytic.ConvergenceRadius` (new file)	1677

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/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.

Decrease in tech debt: (relative, absolute) = (1.00, 0.25)

Current number	Change	Type
4	-1	large files

Current commit a55c588cc0
Reference commit 0eeb5f2502

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).

leanprover-community-bot-assistant · 2025-07-10T19:29:25Z

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

mathlib4-dependent-issues-bot · 2025-07-26T14:50:41Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap #26255~~
By Dependent Issues (🤖). Happy coding!

Ruben-VandeVelde

Seems reasonable, thanks!

maintainer merge

github-actions · 2025-08-15T08:26:55Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

bryangingechen · 2025-08-15T20:47:54Z

Thanks!
bors r+

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors · 2025-08-15T22:00:23Z

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors · 2025-08-15T23:28:06Z

Build failed (retrying...):

CI Success

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors · 2025-08-15T23:34:19Z

This PR was included in a batch that was canceled, it will be automatically retried

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors · 2025-08-16T00:25:38Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

…y#26270) Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

vasnesterov added 12 commits March 4, 2025 12:02

init

d0e8139

long file

8eb9aa6

shake

6ab8fed

Merge branch 'master' into vasnesterov/compContinuousLinearMap

abf6c81

Merge branch 'master' into vasnesterov/compContinuousLinearMap

47d1c35

suggestions

4cf00d9

rename constFormalMultilinearSeries_apply -> constFormalMultilinearSe…

5df46c2

…ries_apply_nonzero

Merge branch 'master' into vasnesterov/compContinuousLinearMap

e03af6b

remove longfile

50da388

Merge branch 'master' into vasnesterov/compContinuousLinearMap

4317214

suggestions

ccc9ee0

split Analytic.Basic

e5eef4a

github-actions bot added t-analysis Analysis (normed *, calculus) large-import Automatically added label for PRs with a significant increase in transitive imports labels Jun 22, 2025

github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Jun 22, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 22, 2025

revert

46035cb

github-actions bot removed large-import Automatically added label for PRs with a significant increase in transitive imports file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels Jun 22, 2025

vasnesterov added 2 commits June 22, 2025 17:12

revert 2

d7c2e4b

porting note

9f9559c

vasnesterov mentioned this pull request Jun 22, 2025

[Merged by Bors] - feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap #26255

Closed

vasnesterov added 2 commits June 22, 2025 17:26

unused import

b34a440

fix

ce3632d

This was referenced Jun 22, 2025

[Merged by Bors] - feat(Analysis/Analytic): HasFPowerSeriesOnBall.compContinuousLinearMap #26268

Closed

feat(Analysis): radius of convergence for binomial series #22538

Closed

noshake

99a3c29

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2025

vasnesterov added 2 commits July 10, 2025 23:19

Merge branch 'master' into split_AnalyticBasic

509534f

merge

23e3c48

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2025

Merge branch 'master' into split_AnalyticBasic

e928c1c

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 26, 2025

vasnesterov added 2 commits July 26, 2025 18:56

revert some

5940d92

update

a55c588

vasnesterov mentioned this pull request Jul 27, 2025

[Merged by Bors] - feat(Analysis): radius of convergence for binomial series #27537

Closed

1 task

vasnesterov added the tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip label Jul 27, 2025

leanprover-community-bot-assistant assigned grunweg Aug 15, 2025

Ruben-VandeVelde approved these changes Aug 15, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 15, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 15, 2025

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

chore(Analysis/Analytic): split Analytic.Basic (#26270)

f91388c

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

chore(Analysis/Analytic): split Analytic.Basic (#26270)

650c7d8

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

chore(Analysis/Analytic): split Analytic.Basic (#26270)

15795d7

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors bot pushed a commit that referenced this pull request Aug 16, 2025

chore(Analysis/Analytic): split Analytic.Basic (#26270)

65eb374

Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.

mathlib-bors bot changed the title ~~chore(Analysis/Analytic): split Analytic.Basic~~ [Merged by Bors] - chore(Analysis/Analytic): split Analytic.Basic Aug 16, 2025

mathlib-bors bot closed this Aug 16, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(Analysis/Analytic): split `Analytic.Basic`#26270

[Merged by Bors] - chore(Analysis/Analytic): split `Analytic.Basic`#26270
vasnesterov wants to merge 23 commits intoleanprover-community:masterfrom
vasnesterov:split_AnalyticBasic

vasnesterov commented Jun 22, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jun 22, 2025 •

edited

Loading

Import changes for modified files

Uh oh!

leanprover-community-bot-assistant commented Jul 10, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jul 26, 2025

Uh oh!

Ruben-VandeVelde left a comment

Uh oh!

github-actions bot commented Aug 15, 2025

Uh oh!

bryangingechen commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

vasnesterov commented Jun 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0eeb5f2502

Import changes for modified files

Declarations diff

Uh oh!

leanprover-community-bot-assistant commented Jul 10, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jul 26, 2025

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 15, 2025

Uh oh!

bryangingechen commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

vasnesterov commented Jun 22, 2025 •

edited

Loading

github-actions bot commented Jun 22, 2025 •

edited

Loading