OAI/GroupTheory/Thompson/AnalyticSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-region uniform separation

The generic results below separate the compactness and scalar estimates from the concrete curve calculations. The actual analytic curve must supply every listed identity and inequality before this result is used in the tube theorem.

  1. theorem OAI.ThompsonNonamenability.Analytic.exists_uniform_sep_on_square line 22
  2. theorem OAI.ThompsonNonamenability.Analytic.uniform_separation_of_five_regions line 54