OAI/GroupTheory/Thompson/AnalyticCurve.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The actual radial oscillating curve

All vectors live in the concrete Euclidean-fiber L² space. The derivative and squared-speed identities are derived from the scalar profiles and the frequency curve, including the profile junctions.

  1. def OAI.ThompsonNonamenability.Analytic.v line 26
  2. def OAI.ThompsonNonamenability.Analytic.gamma line 28
  3. def OAI.ThompsonNonamenability.Analytic.gammaDeriv line 30
  4. def OAI.ThompsonNonamenability.Analytic.u line 33
  5. theorem OAI.ThompsonNonamenability.Analytic.v_norm line 35
  6. theorem OAI.ThompsonNonamenability.Analytic.continuous_v line 37
  7. theorem OAI.ThompsonNonamenability.Analytic.continuous_gamma line 39
  8. theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_v line 41
  9. theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_gamma line 45
  10. theorem OAI.ThompsonNonamenability.Analytic.gamma_norm line 49
  11. theorem OAI.ThompsonNonamenability.Analytic.gamma_zero line 52
  12. theorem OAI.ThompsonNonamenability.Analytic.gamma_of_le_one line 55
  13. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_of_le_one line 58
  14. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_norm_sq line 63
  15. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_speed_lower line 71
  16. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_norm_pos line 81
  17. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_ne_zero line 85
  18. theorem OAI.ThompsonNonamenability.Analytic.u_norm line 88
  19. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_eq_norm_smul_u line 91
  20. theorem OAI.ThompsonNonamenability.Analytic.u_of_le_one line 95
  21. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_inner_v line 99
  22. theorem OAI.ThompsonNonamenability.Analytic.u_inner_v line 105
  23. theorem OAI.ThompsonNonamenability.Analytic.u_inner_v_nonneg line 109
  24. theorem OAI.ThompsonNonamenability.Analytic.v_inner line 113
  25. theorem OAI.ThompsonNonamenability.Analytic.gamma_inner line 116
  26. theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_sq line 121
  27. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_speed_eq_of_le_one line 128
  28. theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_speed_inf line 133