CorrectionLocal.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The local Lipschitz estimate for the explicit tube correction

The radius is the distance to the curve, so its Lipschitz constant is one. The residual itself has local Lipschitz constant eight. Keeping these two estimates separate gives the stated constant for the two cutoff terms.

theorem OAI.ThompsonNonamenability.Analytic.norm_smul_sub_smul_bound line 21
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.residual_radius_lipschitz line 34
Source documentation
The residual length is the actual distance to the curve.
```
theorem residual_radius_lipschitz (x y : C.tube) :
    |‖C.residual x‖ - ‖C.residual y‖| ≤ ‖(x : E) - (y : E)‖ := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.residual_local_bound line 54
Source documentation
Subtracting the nearest curve points costs at most another seven times the distance, on the local parameter-comparison scale.
```
theorem residual_local_bound (x y : C.tube)
    (hxy : ‖(x : E) - (y : E)‖ < C.rho) :
    ‖C.residual x - C.residual y‖ ≤ 8 * ‖(x : E) - (y : E)‖ := by
…
```

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_local_bound line 73

Source documentation

Local Lipschitz control of the actual corrected point.

theorem inside_local_bound (x y : C.tube)
    (hxy : ‖(x : E) - (y : E)‖ < C.rho) :
    ‖D.inside x - D.inside y‖ ≤
      (30 + 7 / (4 * C.rho) + 3808 * C.rho) * ‖(x : E) - (y : E)‖ := by
…