Copyright (c) 2025. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE.

Tubular Neighborhood Projection — Derivative and Main Theorem

Proof that fderiv ℝ π m = V.starProjection at each m ∈ S, and the main theorem assembling all 10 properties of the projection.

theorem PLAcceleratedNesterovLean.tubular_neighborhood_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) : ∃ (π : E → E), (∀ x ∈ U, π x ∈ S ∧ ‖x - π x‖ = Metric.infDist x S) ∧ (∀ x ∈ S, π x = x) ∧ (∀ (x : E), π x ∈ S) ∧ (∀ m ∈ S, ∀ x ∈ U, ‖x - π x‖ ≤ ‖x - m‖) ∧ (∀ m ∈ S, ∃ δ > 0, ∀ x ∈ U, x ∈ Metric.ball m δ → ∀ t ∈ Set.Icc 0 1, (1 - t) • π x + t • x ∈ U) ∧ (∀ x ∈ U, ∀ t ∈ Set.Icc 0 1, have y := (1 - t) • π x + t • x; ‖y - π x‖ = Metric.infDist y S) ∧ (∀ x ∈ U, (fderiv ℝ π (π x)) (x - π x) = 0) ∧ (∀ m ∈ S, DifferentiableAt ℝ π m) ∧ (∀ m ∈ S, ∀ (u v : E), inner ℝ ((fderiv ℝ π m) u) v = inner ℝ u ((fderiv ℝ π m) v)) ∧ ∀ m ∈ S, ContDiffAt ℝ 1 π m