AnalyticTube.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The actual nearest-point parameter on a quantitative curve tube

Compact minimization, stationarity, and the tangent comparison establish existence and uniqueness before the nearest parameter is selected.

theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.nearest_unique line 26
Source documentation
Nearest parameters are unique throughout the metric tube.
```
theorem nearest_unique {x : E} (hx : x ∈ C.tube) {s t : ℝ}
    (hs : C.IsNearest x s) (ht : C.IsNearest x t) : s = t := by
…
```
def OAI.ThompsonNonamenability.Analytic.RegularCurveData.parameter line 40
Source documentation
The unique global nearest parameter, selected after proving attainment.
```
def parameter (x : C.tube) : ℝ :=
…
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.parameter_isNearest line 43
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.parameter_eq_of_isNearest line 46
def OAI.ThompsonNonamenability.Analytic.RegularCurveData.residual line 51
Source documentation
The actual normal residual in the ambient inner-product space.
```
def residual (x : C.tube) : E := (x : E) - C.curve (C.parameter x)
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.curve_add_residual line 53
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.residual_norm line 57
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.residual_norm_lt line 61
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.residual_perp_u line 65
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.parameter_local_bound16 line 69
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.curve_mem_tube line 77
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.parameter_curve line 83
Source documentation
On the curve, the selected nearest parameter is the original parameter.
```
theorem parameter_curve (t : ℝ) :
    C.parameter ⟨C.curve t, C.curve_mem_tube t⟩ = t := by
…
```