OAI/GroupTheory/PolycyclicRecognition/Analysis/CayleyBallCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit word-ball cutoffs and the reverse Poincare inequality

  1. def OAI.PolycyclicRecognition.unitClamp line 10
  2. theorem OAI.PolycyclicRecognition.unitClamp_eq_one line 12
  3. theorem OAI.PolycyclicRecognition.unitClamp_pos_of_ne_zero line 15
  4. theorem OAI.PolycyclicRecognition.unitClamp_nonexpansive line 19
  5. def OAI.PolycyclicRecognition.cayleyBallCutoff line 31
  6. theorem OAI.PolycyclicRecognition.cayleyBallCutoff_eq_one line 34
  7. theorem OAI.PolycyclicRecognition.cayleyBallCutoff_support_neighbor line 42
  8. theorem OAI.PolycyclicRecognition.cayleyBallCutoff_gradient line 56
  9. theorem OAI.PolycyclicRecognition.cayley_wordBall_reverse_poincare line 69