[Merged by Bors] - feat(Topology/Algebra/PontryaginDual): Local Compactness of the Pontryagin Dual

[tb65536]

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

---

• depends on: [Merged by Bors] - feat(Analysis/SpecialFunctions/Complex/Circle): expMapCircle as a PartialHomeomorph and prove IsLocalHomeomorph #11334
• depends on: [Merged by Bors] - feat: general Ascoli theorem #6844
• depends on: [Merged by Bors] - feat(Topology/UniformSpace/Ascoli): Arzela-Ascoli for an equicontinuous family of functions #12002

[github-actions]

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]

Fingers crossed, but I think it's possible there is a big simplification available here in the case of FirstCountableTopology X.

[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]

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

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style