feat: generalize Mathlib.Analysis

[vlad902]

This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.

The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b704.

Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855

---

[vlad902]

!bench

[github-actions]

PR summary 1c2912c3ba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

[j-loreaux]

I stopped reviewing at a certain point. I think some of these are okay, but there are quite a few that I think are not doing anything useful.

Moreover, something about this linter makes me skeptical: it only caught declarations with type class arguments provided explicitly in the declaration (as opposed to in a variable line). This makes me suspect that it didn't look for changes to other declarations (or, if it did, it tried to change variable blocks which failed because some of the declarations needed the existing variables). In either of these cases, I think we shouldn't merge these because it is introducing semi-arbitrary discrepancies in generalization.

[j-loreaux]

This is one of those spurious generalizations. A group with ContinuousAdd and ContinuouSMul is a IsTopologicalAddGroup.

[j-loreaux]

Here and the ones below: EuclideanSpace is only intended to be used for RCLike 𝕜. If someone wants this for a NormedRing 𝕜, then they should use PiLp 𝕜 (n → 𝕜) (or whatever is the correct syntax).

[j-loreaux]

I think this is spurious. IsVonNBounded is only relevant in topological vector spaces.

[leanprover-bot]

Here are the benchmark results for commit 1c2912c.
There were no significant changes against commit 4833c03.

[github-actions]

File	Instructions	%
build	-1.975⬝10⁹	(+0.00%)
Mathlib.Analysis.Matrix	-1.50⬝10⁹	(-1.86%)
CI run

[vlad902]

Closing based on feedback (e.g. see https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2322337.20type.20class.20generalization/with/507342720)