OAI/Probability/FreeIsing/Trees/RestrictedCutCardinality.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.restrictedTreeCut line 9
  2. theorem OAI.Problem367.mem_restrictedTreeCut line 14
  3. theorem OAI.Problem367.card_restrictedTreeCut line 20
  4. def OAI.Problem367.avoidingTreeCut line 25
  5. theorem OAI.Problem367.mem_avoidingTreeCut line 29
  6. theorem OAI.Problem367.card_avoidingTreeCut line 35
  7. theorem OAI.Problem367.pow_le_card_avoidingTreeCut line 40
  8. theorem OAI.Problem367.avoidingTreeCut_nonempty line 46
  9. theorem OAI.Problem367.rpow_le_card_avoidingTreeCut line 53
  10. theorem OAI.Problem367.half_length_rpow_le_card_avoidingTreeCut line 69
  11. theorem OAI.Problem367.attenuation_le_quarter_threshold line 81