OAI/GroupTheory/Thompson/TubeRegularCurve.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ThompsonNonamenability.Analytic.RegularCurveData line 21

   Source documentation

   Differential and separation data at the fixed parameter scale 1 / 32.

   structure RegularCurveData where
   …

2. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.continuous_curve line 42
3. def OAI.ThompsonNonamenability.Analytic.RegularCurveData.rho line 46

   Source documentation

   A radius with slack in both the separation and curvature estimates.

   def rho : ℝ := min (1 / 1024) (C.separation / 8)

4. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.rho_pos line 48
5. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.rho_le line 51
6. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.rho_le_separation line 53
7. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.four_rho_lt_separation line 55
8. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.tangent_error_small line 60
9. def OAI.ThompsonNonamenability.Analytic.RegularCurveData.tube line 65

   Source documentation

   The actual open metric tube around the range of the curve.

   def tube : Set E := {x | Metric.infDist x (range C.curve) < C.rho}

10. theorem OAI.ThompsonNonamenability.Analytic.RegularCurveData.range_nonempty line 67