OAI/GroupTheory/PolycyclicRecognition/Analysis/UnitaryApproximateHarmonic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Almost harmonic unitary cocycles give a nonconstant harmonic function

  1. theorem OAI.PolycyclicRecognition.nonconstant_harmonic_of_almost_harmonic_cocycles line 14