OAI/Probability/CriticalPercolation/Gluing/FreshTrial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BernoulliProduct.allOpen line 15
2. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_allOpen_block line 17
3. lemma OAI.CriticalPercolation.BernoulliProduct.allOpen_inter_lower_le line 31
4. lemma OAI.CriticalPercolation.BernoulliProduct.integrable_blockProbability_real line 59
5. lemma OAI.CriticalPercolation.BernoulliProduct.integral_blockProbability_real line 68
6. theorem OAI.CriticalPercolation.BernoulliProduct.good_trial_bound line 77