OAI/Probability/FreeIsing/Trees/StemRerootAverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.TreeOrbitAverage.stemForbidden line 11
  2. theorem OAI.Problem367.TreeOrbitAverage.card_stemForbidden_le_one line 14
  3. def OAI.Problem367.TreeOrbitAverage.suffixVertex line 19
  4. theorem OAI.Problem367.TreeOrbitAverage.suffixVertex_length line 22
  5. def OAI.Problem367.TreeOrbitAverage.extensionEquivCutDescendants line 25
  6. theorem OAI.Problem367.TreeOrbitAverage.average_extension_suffix line 43
  7. theorem OAI.Problem367.TreeOrbitAverage.stripPrefixAut_extension_prefix line 64
  8. def OAI.Problem367.TreeOrbitAverage.rootEdgeProduct line 81
  9. theorem OAI.Problem367.TreeOrbitAverage.rootEdgeProduct_endpoint_le_rerooted line 85
  10. theorem OAI.Problem367.TreeOrbitAverage.average_rootEdgeProduct_endpoint_le_rerooted line 112