OAI/GroupTheory/Thompson/TubeComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Comparing parameters of nearby normal points

Separation first puts the parameters in the range of the tangent projection estimate. Orthogonality then bounds the remaining projection error by the variation of the tangent. No nearest-point selection is used here.

  1. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.parameter_comparison line 30

    Source documentation

    Normal parameters of two nearby points in the tube satisfy a uniform comparison estimate.

    theorem parameter_comparison (x y : E) (s t : ℝ)
    (hx : ‖x - C.curve s‖ < C.rho) (hy : ‖y - C.curve t‖ < C.rho)
    (hxy : ‖x - y‖ < C.rho)
    (hperp_x : inner (𝕜 := ℝ) (x - C.curve s) (C.tangent s) = 0)
…