feat(Topology/InfiniteSum): applying a tsum of CLM with operator norm

[wwylele]

These three one-liners are provided mostly for discoverability. Especially for ContinuousLinearMap.tsum_apply: when one search for lemma in this shape, they will find tsum_apply which is for pi topology, thus frustratingly not applicable for CLM with operator norm.

I put them in a new file because it imports two somewhat distant files, and I couldn't find a suitable place in existing files

---

[github-actions]

PR summary 8928b411e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.InfiniteSum.Operator (new file)	1694

---

Declarations diff (regex)

+ hasSum_apply
+ summable_apply
+ tsum_apply

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8928b41).

• +3 new declarations
• −0 removed declarations

+ContinuousLinearMap.hasSum_apply
+ContinuousLinearMap.summable_apply
+ContinuousLinearMap.tsum_apply

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 8928b411e5
Reference commit e0c7e5b519

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

[themathqueen]

These should really be for TVS's not just normed spaces. But we don't have a TVS version of apply (i.e., a linear map version: E →ₛₗ[σ] ((E →SL[σ] F) →L[R₂] F)). I'll make a PR for ContinuousLinearMap.applyₗ in a bit. (edit: #43112)

[ADedecker]

Could you try making these lemmas generic over FunLike types with ContinuousEvalConst and the right combination of IsAddApply, IsZeroApply, and so on? I'm not 100% sure it will work nicely, but I think it should be tried.

[ADedecker]

I would also consider renaming tsum_apply to Pi.tsum_apply, maybe in its own preliminary PR?