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

Tubular Neighborhood Projection — Definitions and Helpers

Core definitions (optimalityEqn, IsTubularNeighborhoodOfSubmanifold, tubularProj) and basic helper lemmas for the nearest-point projection.

noncomputable def PLAcceleratedNesterovLean.optimalityEqn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {V : Submodule ℝ E} (φ : ↥V → ↥Vᗮ) (_m : E) : E × ↥V → ↥V

The first-order optimality equation for the nearest-point problem.

Given a submanifold chart (V, φ, δ) at m ∈ S, the nearest point on S to a query point y = m + r is p = m + v + φ(v) where y − p ⊥ T_pS. We encode this as:

F(r, v) = V.orthogonalProjectionOnto(r − v − φ(v)) + (fderiv ℝ φ v).adjoint (V⊥.orthogonalProjectionOnto(r − v − φ(v)))

Equations

• One or more equations did not get rendered due to their size.

structure PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S U : Set E) : Prop

A tubular neighborhood of a C² submanifold S in a finite-dimensional inner product space.

Bundles:

• U is open with S ⊆ U
• Every point in U has a unique nearest point in S
• S is a C² submanifold (locally a C² graph over a subspace)

S is automatically closed relative to U (from uniqueProj); see mem_of_mem_closure_in_U.

• isOpen : IsOpen U
• subset : S ⊆ U
• uniqueProj (x : E) : x ∈ U → ∃! p : E, p ∈ S ∧ dist x p = Metric.infDist x S
• submanifold_chart (m : E) : m ∈ S → ∃ (V : Submodule ℝ E) (φ : ↥V → ↥Vᗮ) (δ : ℝ), 0 < δ ∧ ContDiff ℝ 2 φ ∧ φ 0 = 0 ∧ fderiv ℝ φ 0 = 0 ∧ ∀ x ∈ Metric.ball m δ, x ∈ S ↔ ∃ (v : ↥V), x = m + ↑v + ↑(φ v)

noncomputable def PLAcceleratedNesterovLean.tubularProj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (x : E) : E

The nearest-point projection: for x ∈ U pick the unique closest point in S; for x ∉ U pick an arbitrary element of S.

Equations

• PLAcceleratedNesterovLean.tubularProj hTN hne x = if hx : x ∈ U then Exists.choose ⋯ else hne.some

theorem PLAcceleratedNesterovLean.tubularProj_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (x : E) (hx : x ∈ U) : tubularProj hTN hne x ∈ S ∧ dist x (tubularProj hTN hne x) = Metric.infDist x S

theorem PLAcceleratedNesterovLean.tubularProj_unique {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (x : E) (hx : x ∈ U) (y : E) (hy : y ∈ S ∧ dist x y = Metric.infDist x S) : y = tubularProj hTN hne x

theorem PLAcceleratedNesterovLean.tubularProj_fixes_S {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (x : E) (hx : x ∈ S) : tubularProj hTN hne x = x

theorem PLAcceleratedNesterovLean.fderiv_eq_zero_of_const_on_ray {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → E} {x v : E} (hf : DifferentiableAt ℝ f x) (hfx : f x = x) (hconst : ∀ (t : ℝ), 0 < t → t ≤ 1 → f (x + t • v) = x) : (fderiv ℝ f x) v = 0

If f is differentiable at x, f(x) = x, and f(x + tv) = x for all small t > 0, then fderiv ℝ f x v = 0.

From HasFDerivAt: ‖f(x+h) - x - L(h)‖ ≤ (ε/‖v‖)·‖h‖ for ‖h‖ < δ. Setting h = tv with fiber constancy f(x+tv) = x: t·‖L(v)‖ ≤ (ε/‖v‖)·t·‖v‖ = t·ε, so ‖L(v)‖ ≤ ε. Since ε > 0 is arbitrary, L(v) = 0.

theorem PLAcceleratedNesterovLean.fderiv_eq_zero_of_const_on_ray_local {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → E} {x v : E} (hf : DifferentiableAt ℝ f x) (hfx : f x = x) {t₀ : ℝ} (ht₀ : 0 < t₀) (hconst : ∀ (t : ℝ), 0 < t → t ≤ t₀ → f (x + t • v) = x) : (fderiv ℝ f x) v = 0

Local version: constancy on a short initial segment (0, t₀] suffices.

theorem PLAcceleratedNesterovLean.tubularProj_const_on_fiber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (x : E) (hx : x ∈ U) (t : ℝ) (_ht : t ∈ Set.Icc 0 1) (h_in_U : (1 - t) • tubularProj hTN hne x + t • x ∈ U) (h_realizes : ‖(1 - t) • tubularProj hTN hne x + t • x - tubularProj hTN hne x‖ = Metric.infDist ((1 - t) • tubularProj hTN hne x + t • x) S) : tubularProj hTN hne ((1 - t) • tubularProj hTN hne x + t • x) = tubularProj hTN hne x

π is constant along the fiber segment [(1-t)·πx + t·x] for t ∈ [0,1]. Combines star-shapedness (Prop 5), distance realization (Prop 6), and uniqueness of nearest point.

theorem PLAcceleratedNesterovLean.tubularProj_fiber_realizes_infDist {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) (x : E) (hx : x ∈ U) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖(1 - t) • tubularProj hTN hne x + t • x - tubularProj hTN hne x‖ = Metric.infDist ((1 - t) • tubularProj hTN hne x + t • x) S

The fiber segment from πx to x realizes the infDist at every point. Extracted from the Property 6 proof for reuse in Property 7.

theorem PLAcceleratedNesterovLean.U_isOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) : IsOpen U

U is open.

theorem PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold.mem_of_mem_closure_in_U {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) {x : E} (hxU : x ∈ U) (hx_cl : x ∈ closure S) : x ∈ S

S is closed relative to U: any limit point of S that lies in U belongs to S. Proof: infDist(x, S) = 0 and uniqueProj gives a point of S at distance 0.

theorem PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold.isClosed_inter_closed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) {C : Set E} (hC_closed : IsClosed C) (hC_sub : C ⊆ U) : IsClosed (S ∩ C)

S ∩ C is closed whenever C is closed and C ⊆ U. Follows from S being closed relative to U.

theorem PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold.isCompact_inter_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (hTN : IsTubularNeighborhoodOfSubmanifold S U) [ProperSpace E] {m : E} {r : ℝ} (hr : Metric.closedBall m r ⊆ U) : IsCompact (S ∩ Metric.closedBall m r)

S ∩ closedBall(m, r) is compact when closedBall(m, r) ⊆ U (in a proper metric space).

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

The projection is continuous at every point of S. Since U is open, for m ∈ S ⊆ U, nearby points are in U and dist(π(x), m) ≤ 2·dist(x, m).