feat(Geometry/Manifold): manifolds are locally path-connected

[peabrainiac]

Shows that spaces modelled on locally path-connected spaces are themselves locally path-connected, and that the common model spaces EuclideanHalfSpace n and EuclideanQuadrant n are locally path-connected.

---

• depends on: [Merged by Bors] - feat(Topology/Connected/PathConnected): some instances for locally path-connected spaces #17064
• depends on: [Merged by Bors] - feat(Topology/Connected/PathConnected): some lemmas for pathComponentIn #16983

[github-actions]

PR summary f3395b776c

Import changes exceeding 2%

%	File
+64.56%	Mathlib.Geometry.Manifold.ChartedSpace

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.ChartedSpace	711	1170	+459 (+64.56%)
Mathlib.Analysis.Complex.UpperHalfPlane.Topology	1723	1646	-77 (-4.47%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Complex.UpperHalfPlane.Topology	-77
Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty	-72
Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty	-59
Mathlib.Geometry.Manifold.Sheaf.Basic	443
Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.ChartedSpace	459

---

Declarations diff

+ ChartedSpace.locPathConnectedSpace
+ Convex.locPathConnectedSpace
+ EuclideanHalfSpace.convex
+ EuclideanHalfSpace.pathConnectedSpace
+ EuclideanQuadrant.convex
+ EuclideanQuadrant.pathConnectedSpace
+ instance (priority := 100) LocallyConvexSpace.toLocPathConnectedSpace [Module ℝ E]
+ instance : LocPathConnectedSpace (EuclideanQuadrant n)
+ instance [NeZero n] : LocPathConnectedSpace (EuclideanHalfSpace n)
+ pathComponentIn_mem_nhds
- instance (priority := 100) LocallyConvexSpace.toLocallyConnectedSpace [Module ℝ E]
- instance (priority := 100) NormedSpace.instLocPathConnectedSpace : LocPathConnectedSpace E

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Topology/Connected/PathConnected): some instances for locally path-connected spaces #17064
• [Merged by Bors] - feat(Topology/Connected/PathConnected): some lemmas for pathComponentIn #16983
  By Dependent Issues (🤖). Happy coding!

[peabrainiac]

This should now be up-to-date and free of merge conflicts. There is one thing still left to decide though: should the two instances LocallyConvexSpace.toLocallyConnectedSpace and NormedSpace.instLocPathConnectedSpace that are made redundant by this PR be removed? I assume for LocallyConvexSpace.toLocallyConnectedSpace the answer is yes, since any file that imports it will also have access to instLocallyConnectedSpace (which I realise now should probably be namespaced) and LocallyConvexSpace.toLocPathConnectedSpace from this PR. NormedSpace.instLocPathConnectedSpace is only made redundant by NormedSpace.toLocallyConvexSpace though, which is a bit further up in the import graph; removing it might thus require adding more imports to a few files. I will try to push commits removing those two instances in a moment, and would appreciate feedback on whether those commits should be kept or undone.

[peabrainiac]

Looks like there were actually no further import changes necessary - at least locally, mathlib still built just fine after removing both instances. I'm guessing local path-connectedness of normed spaces wasn't used much yet.

[peabrainiac]

I think I was wrong about Mathlib.Analysis.Convex.Normed not importing Mathlib.Analysis.LocallyConvex.WithSeminorms - I don't know how to check transitive imports like that, and just looked through the direct imports without seeing any connection. Either way though, I think this PR should now be ready for review.