OAI/Probability/FreeIsing/Trees/ColoredEdgeLifts.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.ColoredEdgeLifts.EdgeSpace line 12
  2. def OAI.Problem367.ColoredEdgeLifts.tailLift line 14
  3. theorem OAI.Problem367.ColoredEdgeLifts.tailLift_apply line 34
  4. def OAI.Problem367.ColoredEdgeLifts.reversal line 37
  5. theorem OAI.Problem367.ColoredEdgeLifts.reversal_apply line 40
  6. def OAI.Problem367.ColoredEdgeLifts.headLift line 43
  7. theorem OAI.Problem367.ColoredEdgeLifts.headLift_apply line 46
  8. theorem OAI.Problem367.ColoredEdgeLifts.reversal_tail line 51
  9. theorem OAI.Problem367.ColoredEdgeLifts.reversal_involutive line 54
  10. theorem OAI.Problem367.ColoredEdgeLifts.reversal_head line 60
  11. theorem OAI.Problem367.ColoredEdgeLifts.tailLift_adjoint_apply line 68
  12. theorem OAI.Problem367.ColoredEdgeLifts.tailLift_adjoint_tail line 77
  13. theorem OAI.Problem367.ColoredEdgeLifts.tailLift_adjoint_head line 85
  14. def OAI.Problem367.ColoredEdgeLifts.neighborAverage line 95
  15. theorem OAI.Problem367.ColoredEdgeLifts.neighborAverage_apply line 99
  16. theorem OAI.Problem367.ColoredEdgeLifts.tailLift_adjoint_head_eq_average line 103
  17. def OAI.Problem367.ColoredEdgeLifts.forwardOperator line 108
  18. theorem OAI.Problem367.ColoredEdgeLifts.forwardOperator_apply line 114
  19. theorem OAI.Problem367.ColoredEdgeLifts.isSelfAdjoint_of_involutive line 132
  20. theorem OAI.Problem367.ColoredEdgeLifts.reversal_selfAdjoint line 141
  21. theorem OAI.Problem367.ColoredEdgeLifts.neighborAverage_selfAdjoint line 146