OAI/GroupTheory/Thompson/AnalyticCurveRotation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The explicit orthogonal operators along the actual curve

  1. def OAI.ThompsonNonamenability.Analytic.R line 16
  2. theorem OAI.ThompsonNonamenability.Analytic.R_apply_u line 18
  3. theorem OAI.ThompsonNonamenability.Analytic.R_inner line 21
  4. theorem OAI.ThompsonNonamenability.Analytic.R_norm line 25
  5. theorem OAI.ThompsonNonamenability.Analytic.R_perp line 28
  6. theorem OAI.ThompsonNonamenability.Analytic.R_early line 32
  7. theorem OAI.ThompsonNonamenability.Analytic.R_early_apply line 35
  8. theorem OAI.ThompsonNonamenability.Analytic.lipschitzWith_R line 39
  9. theorem OAI.ThompsonNonamenability.Analytic.R_sub_norm_le line 43