OAI/Probability/CriticalPercolation/ProductMeasure/LevelContactMeasurability.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.finiteSetChoice line 16
  2. lemma OAI.CriticalPercolation.finiteSetChoice_coe line 19
  3. lemma OAI.CriticalPercolation.finiteSetChoice_eq_iff line 22
  4. lemma OAI.CriticalPercolation.measurableSet_set_eq_const line 33
  5. lemma OAI.CriticalPercolation.measurableSet_finiteSetChoice line 43
  6. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_inter_block line 60
  7. lemma OAI.CriticalPercolation.BondGraph.incident_ncard_le line 83
  8. lemma OAI.CriticalPercolation.BondGraph.finite_contactDrop line 96
  9. lemma OAI.CriticalPercolation.BondGraph.contactDrop_ncard_le line 100
  10. lemma OAI.CriticalPercolation.BondGraph.measurable_exteriorCluster line 108
  11. lemma OAI.CriticalPercolation.BondGraph.measurable_levelContacts line 113
  12. lemma OAI.CriticalPercolation.BondGraph.measurable_contactDrop line 122
  13. def OAI.CriticalPercolation.BondGraph.fewContacts line 132
  14. lemma OAI.CriticalPercolation.BondGraph.measurableSet_fewContacts line 135
  15. lemma OAI.CriticalPercolation.BondGraph.fewContacts_finite line 147