OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteGraphCaccioppoli.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-sum reverse energy estimate

The weights will be the adjacency indicators on a finite Cayley ball. The cutoff is supported where the original function is harmonic.

  1. def OAI.PolycyclicRecognition.weightedEdgeSum line 18
  2. theorem OAI.PolycyclicRecognition.weightedEdgeSum_swap line 21
  3. theorem OAI.PolycyclicRecognition.finite_graph_green_identity line 31
  4. theorem OAI.PolycyclicRecognition.finite_graph_caccioppoli line 62