OAI/GroupTheory/PolycyclicRecognition/Analysis/WordBallQuadraticForms.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional function spaces are detected on a word ball

This supplies positivity of the expanding quadratic forms used in the harmonic-function dimension argument.

  1. def OAI.PolycyclicRecognition.wordBallVanishing line 18
  2. theorem OAI.PolycyclicRecognition.wordBallVanishing_antitone line 24
  3. theorem OAI.PolycyclicRecognition.exists_wordBall_detects_finiteDimensional_functions line 29
  4. def OAI.PolycyclicRecognition.wordBallQuadraticValue line 46
  5. theorem OAI.PolycyclicRecognition.wordBallQuadraticValue_nonneg line 49
  6. theorem OAI.PolycyclicRecognition.wordBallQuadraticValue_mono line 52
  7. theorem OAI.PolycyclicRecognition.exists_wordBallQuadraticValue_positive line 57
  8. def OAI.PolycyclicRecognition.wordBallQuadraticForm line 71
  9. theorem OAI.PolycyclicRecognition.wordBallQuadraticForm_apply line 76
  10. theorem OAI.PolycyclicRecognition.exists_wordBallQuadraticForm_posDef line 81