Commit 2025-11-24 19:42 813e2dbe

View on Github →

feat(Algebra/InfiniteSum): HasProdUniformly and friends (#31293) Also refactors HasProdUniformlyOn to take one set instead of a family of sets. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/SummableUniformlyOn/with/553935898

Estimated changes

Modified Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean

modified theorem hasProdUniformlyOn_of_clog

modified theorem multipliableUniformlyOn_of_clog

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

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

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

added theorem HasProdLocallyUniformly.hasProd

added theorem HasProdLocallyUniformly.hasProdLocallyUniformlyOn

added theorem HasProdLocallyUniformly.multipliableLocallyUniformly

added theorem HasProdLocallyUniformly.tendstoLocallyUniformly_finsetRange

added def HasProdLocallyUniformly

added theorem HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn

added theorem HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact

added theorem HasProdLocallyUniformlyOn.mono

modified def HasProdLocallyUniformlyOn

added theorem HasProdUniformly.congr

added theorem HasProdUniformly.hasProd

added theorem HasProdUniformly.hasProdLocallyUniformly

added theorem HasProdUniformly.hasProdUniformlyOn

added theorem HasProdUniformly.multipliableUniformly

added theorem HasProdUniformly.tendstoUniformlyOn_finsetRange

added def HasProdUniformly

modified theorem HasProdUniformlyOn.hasProd

modified theorem HasProdUniformlyOn.hasProdLocallyUniformlyOn

added theorem HasProdUniformlyOn.mono

modified theorem HasProdUniformlyOn.multipliableUniformlyOn

deleted theorem HasProdUniformlyOn.tprod_eq

modified theorem HasProdUniformlyOn.tprod_eqOn

modified def HasProdUniformlyOn

added theorem MultipliableLocallyUniformly.exists

added theorem MultipliableLocallyUniformly.hasProdLocallyUniformly

added theorem MultipliableLocallyUniformly.multipliable

added theorem MultipliableLocallyUniformly.multipliableLocallyUniformlyOn

added def MultipliableLocallyUniformly

added theorem MultipliableLocallyUniformlyOn.exists_multipliableUniformlyOn

added theorem MultipliableLocallyUniformlyOn.mono

added theorem MultipliableLocallyUniformlyOn.multipliableUniformlyOn_of_isCompact

added theorem MultipliableUniformly.exists

added theorem MultipliableUniformly.hasProdUniformly

added theorem MultipliableUniformly.multipliable

added theorem MultipliableUniformly.multipliableUniformlyOn

added def MultipliableUniformly

modified theorem MultipliableUniformlyOn.exists

modified theorem MultipliableUniformlyOn.hasProdUniformlyOn

added theorem MultipliableUniformlyOn.mono

modified theorem MultipliableUniformlyOn.multipliable

modified def MultipliableUniformlyOn

added theorem hasProdLocallyUniformly_iff_tendstoLocallyUniformly

added theorem hasProdLocallyUniformly_of_forall_compact

added theorem hasProdLocallyUniformly_of_of_forall_exists_nhds

modified theorem hasProdUniformlyOn_iff_tendstoUniformlyOn

added theorem hasProdUniformlyOn_univ_iff

added theorem hasProdUniformly_iff_tendstoUniformly

added theorem multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn

added theorem multipliableLocallyUniformly_iff_hasProdLocallyUniformly

added theorem multipliableLocallyUniformly_of_of_forall_exists_nhds

added theorem multipliableUniformlyOn_iff_hasProdUniformlyOn

added theorem multipliableUniformlyOn_univ_iff

added theorem multipliableUniformly_iff_hasProdUniformly