OAI/GroupTheory/PolycyclicRecognition/Analysis/ApproximateHarmonicLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Limits of normalized approximately harmonic functions

Pointwise compactness suffices for the scalar functions obtained by projecting normalized regular-representation coboundaries. In particular, no Hilbert-space ultralimit or nonconstant-harmonic-function existence hypothesis is introduced.

  1. theorem OAI.PolycyclicRecognition.exists_harmonic_limit line 20
  2. theorem OAI.PolycyclicRecognition.exists_nonconstant_polynomial_harmonic_of_approximate line 59