RellichKondrachov.Geometry.Manifold.Riemannian.ChartLocalLipschitzForward #
Local Lipschitz control for the (forward) extended chart on a Riemannian manifold, measured using
riemannianEDist.
Main result #
mfderiv/mfderivWithin takes values in spaces of continuous linear maps between tangent spaces.
For the model space E (viewed as a manifold), we locally activate the NormedAddCommGroup and
NormedSpace instances on its tangent spaces so that operator norms are available (following
Mathlib’s approach in Mathlib.Geometry.Manifold.Riemannian.Basic).
theorem
RellichKondrachov.Geometry.Manifold.Riemannian.lipschitzOnWith_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]
[RegularSpace M]
(x : M)
:
∃ (C : NNReal),
0 < C ∧ ∃ (r : NNReal), 0 < r ∧ LipschitzOnWith C ↑(extChartAt I x) {y : M | Manifold.riemannianEDist I x y < ↑r}
Around any point x, the (forward) extended chart is Lipschitz on a small Riemannian ball
centered at x, with respect to the Riemannian distance.