Commit 2025-08-11 19:22 0a2bda6c

View on Github →

Iterated derivatives of tsum's within some open set. (#26016) We add some IteratedDerivWithin versions of deriv_tsum using the new SummableLocallyUniformly API. This PR continues the work from #25096. Original PR: https://github.com/leanprover-community/mathlib4/pull/25096

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

added theorem eqOn_finsetProd

added theorem eqOn_fun_finsetProd

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

added theorem iteratedDerivWithin_fun_add

Created Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean

added theorem HasSumUniformlyOn.of_norm_le_summable

added theorem HasSumUniformlyOn.of_norm_le_summable_eventually

added theorem SummableLocallyUniformlyOn.of_locally_bounded_eventually

added theorem SummableLocallyUniformlyOn_of_locally_bounded

added theorem derivWithin_tsum

added theorem iteratedDerivWithin_tsum

Modified Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean

added theorem MultipliableLocallyUniformlyOn_congr