feat(Topology/Algebra/PontryaginDual): Local Compactness of the Pontryagin Dual

[tb65536]

This PR uses Arzela-Ascoli to prove local compactness of the Pontryagin dual.

---

• [x] depends on: #11334
• [x] depends on: #6844
• [x] depends on: #12002

[tb65536]

I'm marking this as awaiting-review in case a lemma other than #12002 would be better for this situation.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11334~~
• ~~leanprover-community/mathlib4#6844~~
• ~~leanprover-community/mathlib4#12002~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary 54c5e4f42e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.PontryaginDual	1260	1347	+87 (+6.90%)
Mathlib.Topology.Algebra.ContinuousMonoidHom	1061	1074	+13 (+1.23%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.ContinuousMonoidHom	13
Mathlib.Topology.Algebra.PontryaginDual	87

---

Declarations diff

+ instance [LocallyCompactSpace G] : LocallyCompactSpace (PontryaginDual G) := by + locallyCompactSpace_of_equicontinuousAt + locallyCompactSpace_of_hasBasis

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>

[j-loreaux]

I haven't checked carefully whether these proofs can be significantly simplified, but I don't think it's too big a problem even if they can be.

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style