OAI/Probability/FreeIsing/Trees/SpinEncoding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.spinAgreementCode line 9
  2. lemma OAI.Problem367.spinAgreementCode_injective_right line 12
  3. lemma OAI.Problem367.spinAgreementCode_eq_pos_iff line 17
  4. lemma OAI.Problem367.spinAgreementCode_eq_neg_iff line 21
  5. def OAI.Problem367.connectedSpinEncode line 25
  6. lemma OAI.Problem367.connectedSpinEncode_apply_root line 34
  7. lemma OAI.Problem367.connectedSpinEncode_apply_ne_root line 41
  8. lemma OAI.Problem367.connectedSpinEncode_injective line 51
  9. lemma OAI.Problem367.connectedSpinEncode_bijective line 81
  10. def OAI.Problem367.connectedSpinEquiv line 88
  11. lemma OAI.Problem367.connectedSpinEquiv_apply line 94
  12. lemma OAI.Problem367.spinAgreementCode_comm line 99
  13. lemma OAI.Problem367.ConnectedFinset.spin_eq_on_iff_root_agreements line 103