OAI/Probability/CriticalPercolation/Exploration/AdaptiveReveal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CriticalPercolation.BernoulliProduct.RevealPartition line 14
2. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.cell_measurable line 24
3. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.exists_cell line 27
4. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.cell_unique line 31
5. def OAI.CriticalPercolation.BernoulliProduct.RevealPartition.historySigma line 35
6. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.historySigma_le line 48
7. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.cell_history_measurable line 54
8. def OAI.CriticalPercolation.BernoulliProduct.RevealPartition.probability line 63
9. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.probability_on_cell line 66
10. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.probability_le_one line 77
11. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.probability_measurable line 83
12. theorem OAI.CriticalPercolation.BernoulliProduct.RevealPartition.setLIntegral_probability line 97
13. def OAI.CriticalPercolation.BernoulliProduct.RevealPartition.enlarge line 120
14. def OAI.CriticalPercolation.BernoulliProduct.RevealPartition.decide line 130
15. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.historySigma_le_enlarge line 153
16. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.historySigma_le_decide line 160
17. lemma OAI.CriticalPercolation.BernoulliProduct.RevealPartition.measureReal_inter_le line 170