feat(Analysis/Normed/Group/Ultra): triangle ineq for tsum & tprod

[loefflerd]

---

[github-actions]

PR summary bc3cc9747f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Group.Ultra	1178	1186	+8 (+0.68%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Ring.Ultra	8

---

Declarations diff

+ nnnorm_tprod_le
+ nnnorm_tprod_le_of_forall_le
+ norm_tprod_le
+ norm_tprod_le_of_forall_le
+ norm_tprod_le_of_forall_le_of_nonneg

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.

[pechersky]

Do you think it would be appropriate here to add similar lemmas for `finprod` and `finsum`? You could use the `⨆ (i : s)` syntax to avoid the set-conditionally-complete-lattice problem. Lemmas like `tprod_eq_finprod` could help golf using the lemmas proven here.

…

On Wed, Oct 9, 2024 at 10:18 AM github-actions[bot] < ***@***.***> wrote: PR summary ebfb2f9 <ebfb2f9> Import changes for modified files Dependency changes File Base Count Head Count Change Mathlib.Analysis.Normed.Group.Ultra 1178 1186 +8 (+0.68%) Import changes for all files Files Import difference Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Ring.Ultra 8 ------------------------------ Declarations diff + nnnorm_tprod_le + norm_tprod_le 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. — Reply to this email directly, view it on GitHub <#17584 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABIYHBS2KYO6WLGJWH3CSOTZ2U3LFAVCNFSM6AAAAABPUU5R4CVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMBSGQ4DAMBXGQ> . You are receiving this because your review was requested.Message ID: ***@***.***>

[loefflerd]

Do you think it would be appropriate here to add similar lemmas for finprod and finsum? You could use the ⨆ (i : s) syntax to avoid the set-conditionally-complete-lattice problem. Lemmas like tprod_eq_finprod could help golf using the lemmas proven here.

I thought you might say that 😄 The issue is that we would have multiple formulations to choose from (Finset.sup, Finset.sup', iSup over a subtype, sSup of the range), and I'm not sure which is best. I'd rather not add more API for the finite case in this particular PR; but if you think it's valuable, by all means make a separate PR for it.

In a somewhat opposite direction, I was actually thinking that it might be a good idea to have the tsum/tprod versions of norm_prod_le_of_forall_le_of_nonempty etc.

(As for golfing using tprod_eq_finprod: are you suggesting to derive the finite case from the infinite one? That would probably be circular, since the proof of the tprod result works by applying the prod result to finite sub-products and taking a limit.)