OAI/Probability/CriticalPercolation/ProductMeasure/ForceClosed.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CriticalPercolation.SearchTree.terminalProbability_eq_indicator line 19
2. theorem OAI.CriticalPercolation.SearchTree.contact_normalization line 63
3. def OAI.CriticalPercolation.FiniteProduct.forceClosed line 89
4. lemma OAI.CriticalPercolation.FiniteProduct.forceClosed_normalized line 94
5. lemma OAI.CriticalPercolation.FiniteProduct.forceClosed_nonneg line 102
6. lemma OAI.CriticalPercolation.FiniteProduct.forceClosed_support line 108
7. lemma OAI.CriticalPercolation.FiniteProduct.homogeneous_normalized line 115
8. lemma OAI.CriticalPercolation.FiniteProduct.homogeneous_positive line 122
9. lemma OAI.CriticalPercolation.FiniteProduct.homogeneous_support line 132