OAI/Probability/FreeIsing/Trees/Shells.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.ReducedTail line 9
  2. abbrev OAI.Problem367.TreeShell line 12
  3. instance OAI.Problem367.reducedTailFinite line 14
  4. instance OAI.Problem367.reducedTailFintype line 19
  5. instance OAI.Problem367.treeShellFinite line 22
  6. instance OAI.Problem367.treeShellFintype line 28
  7. def OAI.Problem367.reducedTailSuccEquiv line 31
  8. def OAI.Problem367.treeShellSuccEquiv line 51
  9. def OAI.Problem367.reducedTailZeroEquiv line 68
  10. def OAI.Problem367.treeShellZeroEquiv line 76
  11. theorem OAI.Problem367.card_reducedTail line 85
  12. theorem OAI.Problem367.card_treeShell_zero line 97
  13. theorem OAI.Problem367.card_treeShell_succ line 100
  14. abbrev OAI.Problem367.TreeBall line 105
  15. def OAI.Problem367.treeBallEquivSigma line 107
  16. instance OAI.Problem367.treeBallFinite line 119
  17. instance OAI.Problem367.treeBallFintype line 122
  18. theorem OAI.Problem367.finite_treeShell line 124
  19. theorem OAI.Problem367.finite_treeBall line 127
  20. theorem OAI.Problem367.card_treeBall line 130
  21. def OAI.Problem367.treeShellFinset line 137
  22. def OAI.Problem367.treeBallFinset line 140
  23. theorem OAI.Problem367.mem_treeShellFinset line 143
  24. theorem OAI.Problem367.mem_treeBallFinset line 147
  25. theorem OAI.Problem367.card_treeShellFinset_zero line 151
  26. theorem OAI.Problem367.card_treeShellFinset_succ line 154
  27. theorem OAI.Problem367.card_treeBallFinset line 158
  28. theorem OAI.Problem367.monotone_treeBallFinset line 162
  29. theorem OAI.Problem367.iUnion_treeBallFinset line 166
  30. theorem OAI.Problem367.exists_subset_treeBallFinset line 172
  31. theorem OAI.Problem367.sum_treeShell_succ line 179
  32. theorem OAI.Problem367.sum_reducedTail_succ line 189
  33. theorem OAI.Problem367.sum_treeShell_zero line 199
  34. theorem OAI.Problem367.sum_reducedTail_zero line 206