OAI/GroupTheory/PolycyclicRecognition/Analysis/NormalizedMetricTent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Normalized inverse-coordinate metric cutoffs

  1. def OAI.PolycyclicRecognition.normalizedMetricTent line 17
  2. theorem OAI.PolycyclicRecognition.metricTent_mass_pos line 21
  3. theorem OAI.PolycyclicRecognition.continuous_normalizedMetricTent line 28
  4. theorem OAI.PolycyclicRecognition.normalizedMetricTent_compact_support line 33
  5. theorem OAI.PolycyclicRecognition.normalizedMetricTent_nonneg line 47
  6. theorem OAI.PolycyclicRecognition.integral_normalizedMetricTent line 52
  7. theorem OAI.PolycyclicRecognition.normalizedMetricTent_translation_bound line 60
  8. theorem OAI.PolycyclicRecognition.normalizedMetricTent_translation_support line 79
  9. theorem OAI.PolycyclicRecognition.normalizedMetricTent_translation_integral_le line 105