TubeTangent.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A quantitative lower bound for tangent projections

On a parameter interval of length at most 1 / 32, the velocity has inner product at least 3 / 32 with the tangent at either prescribed endpoint. The scalar mean value theorem then bounds the projected chord from below.

theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.velocity_inner_tangent line 29
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.velocity_tangent_lower line 41
Source documentation
The derivative of projection onto the fixed tangent at s stays positive throughout the prescribed parameter scale.
```
theorem velocity_tangent_lower (s t : ℝ) (hst : |t - s| ≤ 1 / 32) :
    (3 / 32 : ℝ) ≤ inner (𝕜 := ℝ) (C.velocity t) (C.tangent s) := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.tangent_projection_lower line 54
Source documentation
The chord's projection onto the tangent at its first parameter controls parameter distance. The tangent remains fixed at s for either order of s and t.
```
theorem tangent_projection_lower (s t : ℝ) (hst : |t - s| ≤ 1 / 32) :
    (3 / 32 : ℝ) * |t - s| ≤
      |inner (𝕜 := ℝ) (C.curve t - C.curve s) (C.tangent s)| := by
…
```