OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicSpectralSubspace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A large subspace from a determinant bound

If all eigenvalues are at least one and their product is at most K^n, at least half are at most K^2. These coordinates give the controlled-growth subspace used by the harmonic averaging argument.

  1. theorem OAI.PolycyclicRecognition.half_eigenvalues_le_square line 17
  2. def OAI.PolycyclicRecognition.spectralSmallSubspace line 40
  3. def OAI.PolycyclicRecognition.spectralSmallSubspaceEquiv line 46
  4. theorem OAI.PolycyclicRecognition.spectralSmallSubspace_finite line 64
  5. theorem OAI.PolycyclicRecognition.spectralSmallSubspace_finrank line 70
  6. theorem OAI.PolycyclicRecognition.spectralSmallSubspace_dimension line 77
  7. theorem OAI.PolycyclicRecognition.spectralSmallSubspace_quadratic_bound line 83