[Merged by Bors] - feat: TendstoUniformlyOn for tprod's

[CBirkbeck]

Give conditions for prods to converge uniformly to a tprod.

---

• depends on: [Merged by Bors] - feat(Analysis/NormedSpace/FunctionSeries): add eventually versions #16543
• depends on: [Merged by Bors] - feat(Analysis): relate summable and multipliable sequences using log #16546
• depends on: [Merged by Bors] - feat(Topology/UniformSpace/UniformConvergence): add lemma #15398
  

[github-actions]

PR summary 27f6a0ab63

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.SpecialFunctions.Log.Summable	2278	2277	-1 (-0.04%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Log.Summable	-1
Mathlib.Topology.Algebra.InfiniteSum.UniformOn	1
Mathlib.Topology.Algebra.IsUniformGroup.Order (new file)	1033
Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn (new file)	2281

---

Declarations diff

+ HasProdUniformlyOn.hasProdLocallyUniformlyOn
+ HasProdUniformlyOn.tendstoUniformlyOn_finset_range
+ Summable.hasSumUniformlyOn_log_one_add
+ Summable.tendstoUniformlyOn_tsum_nat_log_one_add
+ TendstoUniformlyOn.comp_cexp
+ TendstoUniformlyOn.eventually_forall_le
+ TendstoUniformlyOn.eventually_forall_lt
+ UniformContinuousOn.comp_tendstoUniformlyOn_eventually
+ hasProdLocallyUniformlyOn_nat_one_add
+ hasProdLocallyUniformlyOn_of_forall_compact
+ hasProdLocallyUniformlyOn_one_add
+ hasProdUniformlyOn_nat_one_add
+ hasProdUniformlyOn_of_clog
+ hasProdUniformlyOn_one_add
+ multipliableLocallyUniformlyOn_nat_one_add
+ multipliableLocallyUniformlyOn_one_add
+ multipliableUniformlyOn_nat_one_add
+ multipliableUniformlyOn_of_clog
+ multipliableUniformlyOn_one_add
+ tendstoUniformlyOn_iff_restrict
- Complex.tendstoUniformlyOn_tsum_nat_log_one_add

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).

[loefflerd]

Here are some comments on the files in Topology/. Will look at the analysis files later.

[loefflerd]

I started writing a review and then realised that I had forgotten to update to your latest commits first. Here is what I had up to that point.

[loefflerd]

Thanks for pushing this through!

[loefflerd]

I spotted a few typos which I had overlooked previously (and some golfs in the code which I suggested) so I fixed them and pushed them to your branch. I think this is good now. Thanks for your patience with this!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[CBirkbeck]

No thank you for all the help!

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build