OAI/GroupTheory/Thompson/AnalyticCutoffs.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Scalar cutoffs for the Hilbert displacement construction

The inner cutoff beta is one through radius ρ / 4 and vanishes from ρ / 2. The outer cutoff chi is one through radius ρ / 2 and vanishes from ρ. Both formulas take values in [0, 1] even outside this domain.

  1. def OAI.ThompsonNonamenability.Analytic.beta line 23

    Source documentation

    The cutoff supported inside the half-radius ball.

    def beta (ρ r : ℝ) : ℝ := min 1 (max 0 (2 - 4 * r / ρ))
  2. def OAI.ThompsonNonamenability.Analytic.chi line 26

    Source documentation

    The cutoff supported inside the full-radius ball.

    def chi (ρ r : ℝ) : ℝ := min 1 (max 0 (2 - 2 * r / ρ))
  3. theorem OAI.ThompsonNonamenability.Analytic.beta_nonneg line 28
  4. theorem OAI.ThompsonNonamenability.Analytic.beta_le_one line 31
  5. theorem OAI.ThompsonNonamenability.Analytic.chi_nonneg line 34
  6. theorem OAI.ThompsonNonamenability.Analytic.chi_le_one line 37
  7. theorem OAI.ThompsonNonamenability.Analytic.beta_eq_one line 40
  8. theorem OAI.ThompsonNonamenability.Analytic.beta_eq_zero line 46
  9. theorem OAI.ThompsonNonamenability.Analytic.chi_eq_one line 52
  10. theorem OAI.ThompsonNonamenability.Analytic.chi_eq_zero line 58
  11. theorem OAI.ThompsonNonamenability.Analytic.clamp_abs_sub_le line 64
  12. theorem OAI.ThompsonNonamenability.Analytic.beta_abs_sub_le line 75
  13. theorem OAI.ThompsonNonamenability.Analytic.chi_abs_sub_le line 84
  14. theorem OAI.ThompsonNonamenability.Analytic.beta_le_chi line 93
  15. theorem OAI.ThompsonNonamenability.Analytic.chi_le_tail line 101
  16. theorem OAI.ThompsonNonamenability.Analytic.beta_le_tail line 112