RellichKondrachov.Geometry.Manifold.Riemannian.ChartLocalLipschitz

Local Lipschitz control for Riemannian charts.

This file extracts a reusable lemma showing that, around any point x : M, the inverse extended chart (extChartAt I x).symm is Lipschitz on a small ball in chart coordinates (with respect to the Riemannian edist on M).

Main result

• RellichKondrachov.Geometry.Manifold.Riemannian. lipschitzOnWith_symm_extChartAt_ofRiemannianMetric

mfderivWithin is a continuous linear map between tangent spaces. For the model space E (viewed as a manifold), we locally activate the NormedAddCommGroup/NormedSpace structures on its tangent spaces so that operator-norm estimates are available.

This matches the approach used in Mathlib’s Riemannian manifold development: these instances should not be global because they need not coincide definitionally with Riemannian structures.

theorem RellichKondrachov.Geometry.Manifold.Riemannian.lipschitzOnWith_symm_extChartAt_ofRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [EMetricSpace M] [IsRiemannianManifold I M] (x : M) : ∃ (C : NNReal), 0 < C ∧ ∃ (r : ℝ), 0 < r ∧ LipschitzOnWith C (↑(extChartAt I x).symm) (Metric.ball (↑(extChartAt I x) x) r ∩ Set.range ↑I)

Around any point x, the inverse extended chart is Lipschitz on a small ball in chart coordinates, with respect to the Riemannian distance.