OAI/Probability/CriticalPercolation/Gluing/SelectedFresh.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.block_event_disjoint_forceOn line 15
2. def OAI.CriticalPercolation.BernoulliProduct.selectedEvent line 28
3. lemma OAI.CriticalPercolation.BernoulliProduct.selectedEvent_eq_iUnion line 31
4. lemma OAI.CriticalPercolation.BernoulliProduct.measurableSet_selectedEvent line 37
5. theorem OAI.CriticalPercolation.BernoulliProduct.blockProbability_selected line 43
6. theorem OAI.CriticalPercolation.BernoulliProduct.selected_fresh_bound line 57