OAI/Probability/FreeIsing/Trees/CutContinuations.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.isChain_append_iff_last line 9
  2. def OAI.Problem367.cutLastColor line 22
  3. def OAI.Problem367.appendCutContinuation line 25
  4. def OAI.Problem367.cutPrefix line 31
  5. theorem OAI.Problem367.cutPrefix_appendCutContinuation line 34
  6. def OAI.Problem367.cutSuffix line 41
  7. theorem OAI.Problem367.appendCutContinuation_prefix_suffix line 52
  8. def OAI.Problem367.cutContinuationEquiv line 59
  9. theorem OAI.Problem367.card_cutContinuations line 78
  10. theorem OAI.Problem367.sum_cutContinuations line 82
  11. def OAI.Problem367.cutDescendants line 90
  12. theorem OAI.Problem367.mem_cutDescendants line 95
  13. theorem OAI.Problem367.appendCutContinuation_descendant line 101
  14. theorem OAI.Problem367.sum_cutDescendants line 106
  15. theorem OAI.Problem367.card_cutDescendants line 115
  16. theorem OAI.Problem367.average_cutDescendants line 122
  17. def OAI.Problem367.rootPathVertex line 131
  18. def OAI.Problem367.rootPathProduct line 134
  19. def OAI.Problem367.cutContinuationProduct line 137
  20. theorem OAI.Problem367.rootPathProduct_le_cutContinuationProduct line 142
  21. theorem OAI.Problem367.average_rootPathProduct_le_continuation_average line 157
  22. theorem OAI.Problem367.cutContinuation_vertex_descendant line 171
  23. theorem OAI.Problem367.cutContinuationProduct_congr_on_descendants line 181
  24. theorem OAI.Problem367.shell_head_eq_first line 190
  25. theorem OAI.Problem367.mem_descendants_avoidingTreeCut line 197