OAI/Probability/FreeIsing/Trees/CodedPercolation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.CodedPercolation.incomingEdge line 14
2. def OAI.Problem367.CodedPercolation.incomingLabel line 21
3. theorem OAI.Problem367.CodedPercolation.measurable_incomingLabel line 24
4. theorem OAI.Problem367.CodedPercolation.incoming_all_open line 31
5. def OAI.Problem367.CodedPercolation.openRelation line 56
6. theorem OAI.Problem367.CodedPercolation.measurableSet_openRelation line 60
7. theorem OAI.Problem367.CodedPercolation.openRelation_relabel line 69
8. theorem OAI.Problem367.CodedPercolation.openAdj_incoming_eq line 75
9. theorem OAI.Problem367.CodedPercolation.ae_all_finite_coded_clusters line 92