OAI/GroupTheory/Thompson/AnalyticCurveSeparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform separation of the actual Hilbert-space curve

Every premise of the finite-region separation theorem is proved here from the literal scalar profiles and the oscillator inner-product identity. In particular no separation or injectivity property of the curve is assumed.

  1. theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_of_le_one line 20
  2. theorem OAI.ThompsonNonamenability.Analytic.theta_lt_of_lt_of_one_lt line 27
  3. theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_pos line 36
  4. theorem OAI.ThompsonNonamenability.Analytic.gamma_injective line 55
  5. theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_ge_of_far_negative line 64
  6. theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_sq_tail line 77
  7. theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_sq_ge_of_cross_tail line 85
  8. theorem OAI.ThompsonNonamenability.Analytic.gamma_uniform_separation line 104