TubeNearest.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Global nearest points obtained by compact parameter minimization

No properness of the ambient inner-product space is required. Separation of the curve confines minimization to a compact interval in its real parameter.

def OAI.ThompsonNonamenability.Analytic.RegularCurveData.IsNearest line 27
Source documentation
The predicate of being a global nearest parameter for the actual curve.
```
def IsNearest (x : E) (s : ℝ) : Prop :=
…
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.residual_gt_of_far line 32
Source documentation
The separation estimate makes the residual strictly larger away from a compact interval around any initial tube witness.
```
theorem residual_gt_of_far {x : E} {s t : ℝ}
    (hs : ‖x - C.curve s‖ < C.rho) (hst : (1 / 32 : ℝ) ≤ |t - s|) :
    3 * C.rho < ‖x - C.curve t‖ := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.nearest_exists line 49
Source documentation
A tube point has a global nearest parameter, attained by minimizing on a compact interval of real parameters.
```
theorem nearest_exists (x : E) (hx : x ∈ C.tube) :
    ∃ s : ℝ, C.IsNearest x s ∧ ‖x - C.curve s‖ < C.rho := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.nearest_norm_eq_infDist line 76
Source documentation
Every global minimizer has exactly the distance-to-range residual.
```
theorem nearest_norm_eq_infDist {x : E} {s : ℝ} (hs : C.IsNearest x s) :
    ‖x - C.curve s‖ = Metric.infDist x (range C.curve) := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.nearest_perp_tangent line 87
Source documentation
Differentiating the squared residual at its global minimum proves orthogonality to the tangent.
```
theorem nearest_perp_tangent {x : E} {s : ℝ} (hs : C.IsNearest x s) :
    ⟪x - C.curve s, C.tangent s⟫_ℝ = 0 := by
…
```