OAI/Probability/CriticalPercolation/ProductMeasure/ClosedThin.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteProduct.continuous_prob_weights line 17
2. def OAI.CriticalPercolation.FiniteProduct.closedThin line 27
3. lemma OAI.CriticalPercolation.FiniteProduct.closedThin_zero line 31
4. lemma OAI.CriticalPercolation.FiniteProduct.continuous_closedThin line 36
5. lemma OAI.CriticalPercolation.FiniteProduct.closedThin_mass line 45
6. lemma OAI.CriticalPercolation.FiniteProduct.closedThin_nonneg line 56
7. lemma OAI.CriticalPercolation.FiniteProduct.closedThin_closed_pos line 63
8. lemma OAI.CriticalPercolation.FiniteProduct.prob_mul_le_of_strict line 68