OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicTranslationImage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The maximum principle and the harmonic translation image

A nonconstant harmonic function has infinite translation image. This is the algebraic conclusion needed after constructing a nonconstant Lipschitz harmonic function; no such existence result is assumed here.

  1. theorem OAI.PolycyclicRecognition.cayleyHarmonic_eq_maximum line 16
  2. theorem OAI.PolycyclicRecognition.cayleyHarmonic_finite_range_constant line 41
  3. theorem OAI.PolycyclicRecognition.polynomialHarmonicRepresentation_infinite_range line 55