OAI/GroupTheory/PolycyclicRecognition/Algebra/CayleyDirichletEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Discrete path energy and variance on Cayley balls

These are the finite-sum ingredients of the Cayley-graph Poincare estimate in Kleiner, JAMS 23 (2010), Section 2. No harmonic-function theorem is assumed.

  1. def OAI.PolycyclicRecognition.cayleyDirichletEnergy line 18
  2. theorem OAI.PolycyclicRecognition.cayleyDirichletEnergy_nonneg line 22
  3. theorem OAI.PolycyclicRecognition.cayleyDirichletEnergy_mono line 27
  4. theorem OAI.PolycyclicRecognition.finite_path_energy_bound line 32
  5. theorem OAI.PolycyclicRecognition.sum_pairwise_sq_sub line 42
  6. theorem OAI.PolycyclicRecognition.finite_variance_identity line 50
  7. theorem OAI.PolycyclicRecognition.translated_edge_sum_le_energy line 60
  8. theorem OAI.PolycyclicRecognition.word_path_energy_sum_le line 78