Tubular Neighborhood Projection -- IFT-Based C¹ Regularity

IFT-based proof that the nearest-point projection is C¹ at every point of the submanifold S.

Analysis of fderiv ℝ π x for x ∉ S

At m ∈ S, fderiv ℝ π m = V_m.starProjection (Property 9). But for x ∈ U \ S, the derivative is not simply the orthogonal projection onto the tangent space at π(x). In chart coordinates at m = π(x):

π(y) = m + v*(y − m) + φ(v*(y − m))

where v* : E → V is the IFT solution to the first-order optimality equation F(r, v) = 0. The derivative is:

fderiv ℝ π x = (ι_V + ι_{V⊥} ∘ Dφ(v₀)) ∘ Dv*(r₀)

where v₀ = v*(x − m), r₀ = x − m, and Dv* is given by the implicit derivative formula Dv* = −(∂F/∂v)⁻¹ ∘ (∂F/∂r).

At v₀ = 0 (i.e., x = m ∈ S), Dφ(0) = 0 and Dv*(0) = proj_V, recovering fderiv ℝ π m = V.starProjection.

At v₀ ≠ 0, Dφ(v₀) ≠ 0, and the derivative depends on second-order geometry (D²φ) of the submanifold. Continuity of x ↦ fderiv ℝ π x follows from the IFT giving C¹ regularity of v*.

Why the IFT is essential: To determine fderiv ℝ π x at x ∉ S, one must solve the optimality equation (which IS the IFT). Composing x ↦ π(x) ↦ V_{π(x)} ↦ V_{π(x)}.starProjection only gives the derivative on S; the IFT extends it to all of U.

theorem PLAcceleratedNesterovLean.optimalityEqn_contDiff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {V : Submodule ℝ E} {φ : ↥V → ↥Vᗮ} (hφ : ContDiff ℝ 2 φ) (m : E) : ContDiff ℝ 1 (optimalityEqn φ m)

theorem PLAcceleratedNesterovLean.optimalityEqn_partial_v_eq_neg_id {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {V : Submodule ℝ E} {φ : ↥V → ↥Vᗮ} (hφC2 : ContDiff ℝ 2 φ) (hφ0 : φ 0 = 0) (hDφ0 : fderiv ℝ φ 0 = 0) (m : E) : fderiv ℝ (optimalityEqn φ m) (0, 0) ∘SL ContinuousLinearMap.inr ℝ E ↥V = -ContinuousLinearMap.id ℝ ↥V

At the base point (0, 0), ∂F/∂v = −Id_V.

More precisely: F(r, v) = T_v*(r − v − φ(v)) and at v = 0:

• T_0 = ι_V (since Dφ(0) = 0), so T_0* = V.orthogonalProjectionOnto
• ∂/∂v [r − v − φ(v)]|_{v=0} = −Id − Dφ(0) = −Id
• ∂F/∂v|_{(r,0)} = T_0*(−Id) + [D_v T_v*]·(r − 0 − 0) = −Id_V + ...

The second term involves D²φ(0) contracted with the normal component of r. At r = 0, it vanishes, giving ∂F/∂v = −Id_V.

At general (r₀, v₀): ∂F/∂v = −(Id_V + Dφ(v₀)* ∘ Dφ(v₀)) + [D²φ-dependent terms]

The operator Id_V + Dφ(v₀)* ∘ Dφ(v₀) is always positive definite (≥ Id_V). The D²φ terms are bounded by ‖D²φ‖ · ‖normal distance‖. Within the tube (radius < reach), this perturbation is small enough that ∂F/∂v remains invertible.

theorem PLAcceleratedNesterovLean.optimalityEqn_partial_v_bijective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {V : Submodule ℝ E} {φ : ↥V → ↥Vᗮ} (hφC2 : ContDiff ℝ 2 φ) (hφ0 : φ 0 = 0) (hDφ0 : fderiv ℝ φ 0 = 0) (m : E) : have F' := fderiv ℝ (optimalityEqn φ m) (0, 0); Function.Bijective ⇑(F' ∘SL ContinuousLinearMap.inr ℝ E ↥V)

theorem PLAcceleratedNesterovLean.localMin_sq_dist_implies_optimalityEqn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {V : Submodule ℝ E} {φ : ↥V → ↥Vᗮ} (hφC2 : ContDiff ℝ 2 φ) (m : E) {r : E} {v' : ↥V} (h_min : IsLocalMin (fun (v : ↥V) => ‖r - ↑v - ↑(φ v)‖ ^ 2) v') : optimalityEqn φ m (r, v') = 0

If v' locally minimizes g(v) = ‖r - v↑ - (φ v)↑‖², then F(r, v') = 0.

theorem PLAcceleratedNesterovLean.tubularProj_contDiffAt_S {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (m : E) (hm : m ∈ S) : ContDiffAt ℝ 1 (tubularProj hTN hne) m

For each m ∈ S, the nearest-point projection π is C¹ at m.

Proof strategy (Foote 1984, adapted): Apply the IFT at (0, 0) where ∂F/∂v = −Id is bijective by optimalityEqn_partial_v_bijective. Get a C¹ implicit function v* near 0. Use continuity of π and IFT uniqueness to show π = χ near m, where χ(y) = m + v*(y−m) + φ(v*(y−m)) is C¹.