OAI/Probability/CriticalPercolation/ProductMeasure/LayerExpectation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.vertexCount line 16
  2. lemma OAI.CriticalPercolation.vertexCount_finite line 18
  3. lemma OAI.CriticalPercolation.vertexCount_mono line 30
  4. lemma OAI.CriticalPercolation.measurable_vertexCount line 37
  5. lemma OAI.CriticalPercolation.lintegral_vertexCount line 43
  6. def OAI.CriticalPercolation.BondGraph.seedExpectation line 57
  7. def OAI.CriticalPercolation.BondGraph.goodEntrySeeds line 60
  8. lemma OAI.CriticalPercolation.BondGraph.measurableSet_goodEntrySeed line 63
  9. lemma OAI.CriticalPercolation.BondGraph.lintegral_entrySeeds line 77
  10. lemma OAI.CriticalPercolation.BondGraph.subcritical_seedExpectation_bound line 82
  11. lemma OAI.CriticalPercolation.BondGraph.seedExpectation_self_le line 99
  12. lemma OAI.CriticalPercolation.BondGraph.expected_goodSeeds_lower line 109
  13. lemma OAI.CriticalPercolation.BondGraph.expected_layer_expansion line 134