[Merged by Bors] - Iterated derivatives of tsum's within some open set.

[CBirkbeck]

We add some IteratedDerivWithin versions of deriv_tsum using the new SummableLocallyUniformly API.

This PR continues the work from #25096.

Original PR: #25096

[CBirkbeck]

Comments from Original PR #25096

This section contains 1 comment(s) from the original PR, excluding bot comments.

---

@github-actions (2025-05-21 21:13 UTC):

PR summary 9a0f6ccbc2

Import changes exceeding 2%

%	File
+27.15%	Mathlib.Analysis.NormedSpace.FunctionSeries

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.NormedSpace.FunctionSeries	1370	1742	+372 (+27.15%)

Import changes for all files

Files	Import difference
30 files Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.Harmonic.ZetaAsymp 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.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.ZMod 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	1
68 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.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.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation 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.Log.Summable Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.NumberField.AdeleRing 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.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator 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	2
Mathlib.Analysis.Fourier.RiemannLebesgueLemma	8
Mathlib.Geometry.Manifold.Metrizable	32
10 files Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.DistribChar Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.NumberTheory.WellApproximable	51
Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real	53
Mathlib.Analysis.Complex.Tietze	70
Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence	74
Mathlib.Topology.ContinuousMap.Ideals	78
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic	123
Mathlib.FieldTheory.Galois.Profinite	148
Mathlib.Topology.Separation.NotNormal Mathlib.Topology.TietzeExtension	162
Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling	195
Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Topology.MetricSpace.PartitionOfUnity	213
11 files Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Solid	216
Mathlib.Condensed.Limits Mathlib.Condensed.Module	220
Mathlib.Topology.Category.Profinite.Nobeling.Successor	221
Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit	243
Mathlib.Topology.Category.Profinite.Nobeling.Span	247
Mathlib.MeasureTheory.Measure.EverywherePos	248
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Category.Profinite.Nobeling.Basic	249
30 files Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Equivalence Mathlib.Condensed.Functors Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits	250
8 files Mathlib.Condensed.TopCatAdjunction Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Locale Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.Order.Category.FrameAdjunction	253
Mathlib.Topology.Separation.CompletelyRegular	254
5 files Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.TopComparison Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.PartitionOfUnity	255
6 files Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma	256
Mathlib.Analysis.NormedSpace.FunctionSeries	372

---

Declarations diff

+ HasSumUniformlyOn_of_bounded
+ HasSumUniformlyOn_of_cofinite_eventually
+ SummableLocallyUniformlyOn.of_locally_bounded
+ derivWithin_tsum

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 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 summary 138b030bbf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (new file)	1800

---

Declarations diff

+ HasSumUniformlyOn.of_norm_le_summable
+ HasSumUniformlyOn.of_norm_le_summable_eventually
+ MultipliableLocallyUniformlyOn_congr
+ SummableLocallyUniformlyOn.of_locally_bounded_eventually
+ SummableLocallyUniformlyOn_of_locally_bounded
+ derivWithin_tsum
+ eqOn_finsetProd
+ eqOn_fun_finsetProd
+ iteratedDerivWithin_fun_add
+ iteratedDerivWithin_tsum

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 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]

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

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[CBirkbeck]

bors r+

[mathlib-bors]

Canceled.

[CBirkbeck]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success