OAI/Probability/CriticalPercolation/GraphGeometry/HitEvent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BondGraph.hitEvent line 24
  2. lemma OAI.CriticalPercolation.BondGraph.measurableSet_hitEvent line 27
  3. lemma OAI.CriticalPercolation.BondGraph.hitEvent_mono_edges line 31
  4. lemma OAI.CriticalPercolation.BondGraph.hitEvent_mono_target line 35
  5. lemma OAI.CriticalPercolation.BondGraph.expect_hit_eq_real line 39
  6. lemma OAI.CriticalPercolation.BondGraph.expect_jointHit_eq_real line 53
  7. lemma OAI.CriticalPercolation.BondGraph.finite_edge_joint_gluing_law line 67
  8. def OAI.CriticalPercolation.BondGraph.restrictEdges line 79
  9. lemma OAI.CriticalPercolation.BondGraph.restrictEdges_openGraph line 82
  10. lemma OAI.CriticalPercolation.BondGraph.restrictEdges_hitEvent line 94
  11. lemma OAI.CriticalPercolation.BondGraph.finite_subgraph_joint_gluing line 102
  12. lemma OAI.CriticalPercolation.BondGraph.finite_subset_exhaustion line 126
  13. lemma OAI.CriticalPercolation.BondGraph.hitEvent_exhaustion line 140
  14. lemma OAI.CriticalPercolation.BondGraph.hitEvent_exhaustion_mono line 154
  15. lemma OAI.CriticalPercolation.BondGraph.tendsto_real_hitEvent_exhaustion line 160
  16. lemma OAI.CriticalPercolation.BondGraph.jointHitEvent_exhaustion line 170
  17. lemma OAI.CriticalPercolation.BondGraph.tendsto_real_jointHitEvent_exhaustion line 181
  18. lemma OAI.CriticalPercolation.BondGraph.finite_sum_abs_sub_bound line 192
  19. lemma OAI.CriticalPercolation.BondGraph.countable_joint_gluing_finite line 196
  20. lemma OAI.CriticalPercolation.BondGraph.hitEvent_iUnion line 232
  21. theorem OAI.CriticalPercolation.BondGraph.countable_joint_gluing line 243
  22. theorem OAI.CriticalPercolation.BondGraph.joint_gluing line 272