OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteUnitaryAverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite simultaneous averages in a unitary representation

Each finite convex averaging operator is a contraction. Successively averaging each of finitely many vectors preserves all earlier bounds. This is the Hilbert averaging step used for the abelian cohomology base case.

  1. def OAI.PolycyclicRecognition.FiniteOrbitAverage.onVector line 21
  2. theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.onVector_sub line 24
  3. theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.norm_onVector_le line 29
  4. theorem OAI.PolycyclicRecognition.exists_finiteVectorAverage line 39
  5. def OAI.PolycyclicRecognition.FiniteOrbitAverage.compose line 56
  6. theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.compose_onVector line 63
  7. theorem OAI.PolycyclicRecognition.zero_mem_unitaryOrbitHull line 72
  8. theorem OAI.PolycyclicRecognition.exists_small_convex_unitaryOrbit line 79
  9. theorem OAI.PolycyclicRecognition.exists_unitaryAverage_small_finset line 86
  10. theorem OAI.PolycyclicRecognition.exists_unitaryAverage_small_finite line 113