OAI/Probability/CriticalPercolation/Entropy/BinaryMarks.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BinaryLaw.nodeMark line 15
2. lemma OAI.CriticalPercolation.BinaryLaw.nodeMark_old line 19
3. lemma OAI.CriticalPercolation.BinaryLaw.nodeMark_current line 23
4. lemma OAI.CriticalPercolation.BinaryLaw.canonical_append_iff line 26
5. lemma OAI.CriticalPercolation.BinaryLaw.current_mark_geometry line 42
6. lemma OAI.CriticalPercolation.BinaryLaw.current_canonical_iff line 70
7. lemma OAI.CriticalPercolation.BinaryLaw.canonical_iff_nonhold line 103
8. lemma OAI.CriticalPercolation.BinaryLaw.node_mark_geometry line 120
9. lemma OAI.CriticalPercolation.BinaryLaw.canonical_node_reachable_eq line 140
10. lemma OAI.CriticalPercolation.BinaryLaw.selected_marks_injective line 147
11. def OAI.CriticalPercolation.BinaryLaw.activeNodes line 174
12. lemma OAI.CriticalPercolation.BinaryLaw.active_lt line 179
13. lemma OAI.CriticalPercolation.BinaryLaw.active_canonical line 194
14. lemma OAI.CriticalPercolation.BinaryLaw.active_nonhold line 208