Commit 2025-05-13 22:40 7ae6f6a7

View on Github →

feat(Topology/Algebra/InfiniteSum): uniform summability (#23507) Define summability / multipliability uniformly on a set, or locally uniformly.

Estimated changes

Modified Mathlib.lean

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

added theorem HasProdLocallyUniformlyOn.hasProd

added theorem HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn

added theorem HasProdLocallyUniformlyOn.tprod_eqOn

added def HasProdLocallyUniformlyOn

added theorem HasProdUniformlyOn.hasProd

added theorem HasProdUniformlyOn.multipliableUniformlyOn

added theorem HasProdUniformlyOn.tprod_eq

added theorem HasProdUniformlyOn.tprod_eqOn

added def HasProdUniformlyOn

added theorem MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn

added theorem MultipliableLocallyUniformlyOn.multipliable

added def MultipliableLocallyUniformlyOn

added theorem MultipliableUniformlyOn.exists

added theorem MultipliableUniformlyOn.hasProdUniformlyOn

added theorem MultipliableUniformlyOn.multipliable

added def MultipliableUniformlyOn

added theorem hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn

added theorem hasProdLocallyUniformlyOn_of_of_forall_exists_nhd

added theorem hasProdUniformlyOn_iff_tendstoUniformlyOn

added theorem multipliableLocallyUniformlyOn_of_of_forall_exists_nhd

Modified Mathlib/Topology/Algebra/UniformConvergence.lean

added theorem UniformFun.ofFun_prod

added theorem UniformFun.toFun_prod

added theorem UniformOnFun.ofFun_prod

added theorem UniformOnFun.toFun_prod

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean

added theorem tendstoLocallyUniformlyOn_of_forall_exists_nhd

added theorem tendstoLocallyUniformly_of_forall_exists_nhd