feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas

[Jun2M]

Following the PR #38489, this PR add deprecated tags to the original ENNReal lemmas and change the transitive children files to use the generalized lemmas rather than the deprecated lemmas.

Related Zulip thread: #Is there code for X? > Summing ENats without topology

---

• depends on: feat(Topology/Algebra/InfiniteSum): Generalize ENNReal lemmas #38489

[github-actions]

PR summary 9268b22206

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.InfiniteSum.Order	1174	1178	+4 (+0.34%)

Import changes for all files

Files	Import difference
8 files Mathlib.Analysis.Asymptotics.Completion Mathlib.Analysis.NormedSpace.Connected Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.NumberTheory.TsumDivsorsAntidiagonal Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.Compactness.HilbertCubeEmbedding Mathlib.Topology.Instances.Real.Lemmas Mathlib.Topology.Semicontinuous	4

---

Declarations diff

+ CompleteLattice.hasProd
+ CompleteLattice.multipliable
+ le_tprod
+ le_tprod_of_mem
+ ne_top_of_tprod_ne_top
+ prod_le_tprod
+ prod_mul_tprod_compl
+ tprod_biUnion
+ tprod_biUnion'
+ tprod_biUnion_le
+ tprod_biUnion_le_tprod
+ tprod_comm
+ tprod_comp_eq_tprod_of_bijective
+ tprod_comp_eq_tprod_of_equiv
+ tprod_comp_le_tprod_of_injective
+ tprod_eq_iSup_prod
+ tprod_eq_iSup_prod'
+ tprod_eq_mul_tprod_ite
+ tprod_eq_top_of_eq_top
+ tprod_eq_zero
+ tprod_fiberwise
+ tprod_iUnion_eq_tprod
+ tprod_iUnion_le
+ tprod_iUnion_le_tprod
+ tprod_insert
+ tprod_le_of_subset
+ tprod_le_tprod
+ tprod_le_tprod_comp_of_surjective
+ tprod_mono_subtype
+ tprod_mul
+ tprod_prod
+ tprod_prod'
+ tprod_sigma
+ tprod_sigma'
+ tprod_singleton_mul_tprod_ne
+ tprod_subtype_eq_top_of_eq_top
+ tprod_top
+ tprod_union_disjoint
+ tprod_union_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[SnirBroshi]

This is amazing but I fear it's too big for review. Is it possible to split the generalization from refactoring all of the files? If not, then perhaps you could add the generalized proofs without removing the ENNReal ones, and only later remove and refactor?

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Topology/Algebra/InfiniteSum): Generalize ENNReal lemmas #38489
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.