OAI/GroupTheory/PolycyclicRecognition/Analysis/SmallCoefficientRationalMean.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An invariant rational functional on the rationalized coefficient ring

The real mean proves that the constant class is nonzero in coinvariants. Linear separation over the rationals then supplies a rational functional; no rational-valued positive mean on all bounded functions is assumed.

  1. abbrev OAI.PolycyclicRecognition.SmallCoefficientRationalSpace line 21
  2. def OAI.PolycyclicRecognition.smallCoefficientRationalAction line 23
  3. def OAI.PolycyclicRecognition.smallCoefficientRationalRealMean line 39
  4. theorem OAI.PolycyclicRecognition.smallCoefficientRationalRealMean_invariant line 43
  5. def OAI.PolycyclicRecognition.smallCoefficientRealCoinvariantMean line 51
  6. theorem OAI.PolycyclicRecognition.smallCoefficientRealCoinvariantMean_one line 57
  7. theorem OAI.PolycyclicRecognition.exists_smallCoefficient_rational_mean line 64