OAI/Probability/FreeIsing/Trees/Regularity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.treeStep line 8
  2. theorem OAI.Problem367.treeStep_adj line 22
  3. theorem OAI.Problem367.treeStep_injective line 32
  4. theorem OAI.Problem367.treeStep_eq_iff line 48
  5. theorem OAI.Problem367.treeStep_involutive line 73
  6. theorem OAI.Problem367.treeAdj_iff_exists_treeStep line 79
  7. def OAI.Problem367.treeNeighborEquiv line 88
  8. instance OAI.Problem367.treeNeighborsFinite line 98
  9. theorem OAI.Problem367.card_treeNeighbors line 102
  10. def OAI.Problem367.treeNeighborFinset line 107
  11. theorem OAI.Problem367.mem_treeNeighborFinset line 111
  12. theorem OAI.Problem367.card_treeNeighborFinset line 116
  13. theorem OAI.Problem367.treeStep_length line 122
  14. theorem OAI.Problem367.sum_treeNeighborFinset_radial line 128