OAI/Probability/CriticalPercolation/ProductMeasure/Delta.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteProduct.expect_eval_indicator line 16
2. lemma OAI.CriticalPercolation.FiniteProduct.expect_coordinate_mask line 39
3. lemma OAI.CriticalPercolation.FiniteProduct.expect_pin_eq_force line 75
4. lemma OAI.CriticalPercolation.FiniteProduct.expect_pin_transport line 81
5. lemma OAI.CriticalPercolation.FiniteProduct.prob_congr_support line 87
6. lemma OAI.CriticalPercolation.FiniteProduct.prob_pin_transport line 93
7. def OAI.CriticalPercolation.FiniteProduct.delta line 98
8. def OAI.CriticalPercolation.FiniteProduct.openPivot line 101
9. lemma OAI.CriticalPercolation.FiniteProduct.openPivot_force_true line 105
10. lemma OAI.CriticalPercolation.FiniteProduct.delta_eq_pivotal line 112