OAI/GroupTheory/Thompson/AnalyticPlaneOscillator.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean planar oscillator

The ordinary sine/cosine circle and its tangent have unit Euclidean norm. The derivative of the tangent is the negative circle vector. The mean value inequality therefore gives Lipschitz constant one for both functions, and a quadratic first-order remainder estimate with constant one.

  1. def OAI.ThompsonNonamenability.Analytic.planeWave line 25
  2. def OAI.ThompsonNonamenability.Analytic.planeDeriv line 27
  3. theorem OAI.ThompsonNonamenability.Analytic.planeWave_norm line 29
  4. theorem OAI.ThompsonNonamenability.Analytic.planeDeriv_norm line 33
  5. theorem OAI.ThompsonNonamenability.Analytic.planeWave_inner_planeDeriv line 37
  6. theorem OAI.ThompsonNonamenability.Analytic.planeWave_inner line 42
  7. theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_planePair line 47
  8. theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_planeWave line 58
  9. theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_planeDeriv line 62
  10. theorem OAI.ThompsonNonamenability.Analytic.continuous_planeWave line 71
  11. theorem OAI.ThompsonNonamenability.Analytic.continuous_planeDeriv line 74
  12. theorem OAI.ThompsonNonamenability.Analytic.planeWave_sub_norm_le line 77
  13. theorem OAI.ThompsonNonamenability.Analytic.planeDeriv_sub_norm_le line 86
  14. theorem OAI.ThompsonNonamenability.Analytic.planeWave_remainder line 95