feat(Logic/Equiv/Basic): sumSigmaDistrib, finSigmaFinEquiv

[Timeroot]

Upstreamed from the EquationalTheories project.

[github-actions]

PR summary 9fcfebfbc1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ finSigmaFinEquiv
+ finSigmaFinEquiv_apply
+ finSigmaFinEquiv_one
+ sumSigmaDistrib
+ uniqueSigma
+ uniqueSigma_apply
+ uniqueSigma_symm_apply

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

[quangvdao]

I also defined finSigmaFinEquiv in another PR #19013, but this definition looks a lot neater than mine.

[Timeroot]

I also defined finSigmaFinEquiv in another PR #19013, but this definition looks a lot neater than mine.

Oh haha! When I was writing mine (which was pretty much the exact same time as you writing yours) I checked loogle/mathlib but not the current PRs.

I guess it's a testament to Mathlib's naming convention, that two of us could write totally separate implementations of the same idea, that do the exact same thing, with the exact same name.

[jcommelin]

Could you please provide a few API lemmas that will help working with this defn?

[Timeroot]

I added finSigmaFinEquiv_apply and finSigmaFinEquiv_one. I would add finSigmaFinEquiv_symm_apply but I don't think there's a particularly clean statement of the inverse equivalence (at least, not clean enough to be useful - I think the forward apply should be preferred)

[quangvdao]

Note that there's WIP in Batteries to provide a more cohesive framework for Fin equivalences: leanprover-community/batteries#1007.

My PR also defines auxiliary functions that explicitly identify the inverse equivalence #19013.

[Timeroot]

I see, I guess one can write it in terms of these divSum and modSum you defined. Well, I guess we both have definitions of this equivalence. I'll leave mine like this (without a the _symm_apply lemma), I'm fine with either definition getting merged. #19695 just requires some definition of finSigmaFinEquiv.

[quangvdao]

I'm also fine with either definitions, and wonder if we could have the best of both worlds (explicit formulas from my PR, plus theorems that relate it to your PR).

[jcommelin]

Apart from one comment, LGTM