OAI/GroupTheory/PolycyclicRecognition/Analysis/MetricTent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Compact metric cutoffs for controlled Følner pairs

  1. def OAI.PolycyclicRecognition.metricTent line 18
  2. theorem OAI.PolycyclicRecognition.metricTent_nonneg line 20
  3. theorem OAI.PolycyclicRecognition.metricTent_le_one line 23
  4. theorem OAI.PolycyclicRecognition.metricTent_eq_one line 29
  5. theorem OAI.PolycyclicRecognition.continuous_metricTent line 32
  6. theorem OAI.PolycyclicRecognition.abs_metricTent_sub_le line 35
  7. theorem OAI.PolycyclicRecognition.metricTent_support_subset line 48
  8. theorem OAI.PolycyclicRecognition.metricTent_compact_support line 58
  9. theorem OAI.PolycyclicRecognition.metricTent_integral_lower line 67