Commit 2025-06-02 15:20 2bf9d215

View on Github →

feat: TendstoUniformlyOn for tprod's (#13349) Give conditions for prods to converge uniformly to a tprod.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/FunctionSeries.lean

Created Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean

added theorem Summable.hasProdLocallyUniformlyOn_nat_one_add

added theorem Summable.hasProdLocallyUniformlyOn_one_add

added theorem Summable.hasProdUniformlyOn_nat_one_add

added theorem Summable.hasProdUniformlyOn_one_add

added theorem Summable.hasSumUniformlyOn_log_one_add

added theorem Summable.multipliableLocallyUniformlyOn_nat_one_add

added theorem Summable.multipliableLocallyUniformlyOn_one_add

added theorem Summable.multipliableUniformlyOn_nat_one_add

added theorem Summable.multipliableUniformlyOn_one_add

added theorem Summable.tendstoUniformlyOn_tsum_nat_log_one_add

added theorem TendstoUniformlyOn.comp_cexp

added theorem hasProdUniformlyOn_of_clog

added theorem multipliableUniformlyOn_of_clog

Modified Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

deleted theorem Complex.multipliable_one_add_of_summable

deleted theorem Complex.tendstoUniformlyOn_tsum_nat_log_one_add

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

added theorem HasProdUniformlyOn.hasProdLocallyUniformlyOn

added theorem HasProdUniformlyOn.tendstoUniformlyOn_finset_range

added theorem hasProdLocallyUniformlyOn_of_forall_compact

Created Mathlib/Topology/Algebra/IsUniformGroup/Order.lean

added theorem TendstoUniformlyOn.eventually_forall_le

added theorem TendstoUniformlyOn.eventually_forall_lt

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean

added theorem tendstoUniformlyOn_iff_restrict

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

modified theorem UniformContinuousOn.comp_tendstoUniformly

added theorem UniformContinuousOn.comp_tendstoUniformlyOn_eventually

modified theorem UniformContinuousOn.comp_tendstoUniformly_eventually