OAI/Probability/BenjaminiSchramm/LayerFrontierGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Percolation.BenjaminiSchramm.openFrontier line 16
  2. lemma OAI.Percolation.BenjaminiSchramm.openFrontier_dependsOn line 19
  3. lemma OAI.Percolation.BenjaminiSchramm.openFrontier_finite line 29
  4. lemma OAI.Percolation.BenjaminiSchramm.measurable_mem_openFrontier line 35
  5. lemma OAI.Percolation.BenjaminiSchramm.measurableSet_openFrontier_eq line 40
  6. lemma OAI.Percolation.BenjaminiSchramm.restricted_exactCluster_dependsOn line 51
  7. lemma OAI.Percolation.BenjaminiSchramm.measurableSet_restricted_exactCluster line 64
  8. def OAI.Percolation.BenjaminiSchramm.lowerFrontierCell line 72
  9. lemma OAI.Percolation.BenjaminiSchramm.lowerFrontierCell_dependsOn line 75
  10. lemma OAI.Percolation.BenjaminiSchramm.measurableSet_lowerFrontierCell line 91
  11. theorem OAI.Percolation.BenjaminiSchramm.conn_last_exit_frontier line 99
  12. lemma OAI.Percolation.BenjaminiSchramm.openFrontier_lowerCluster_outside line 118
  13. theorem OAI.Percolation.BenjaminiSchramm.lowerCluster_new_vertex_cover line 127
  14. def OAI.Percolation.BenjaminiSchramm.restrictedLayerCount line 136
  15. lemma OAI.Percolation.BenjaminiSchramm.measurable_restrictedLayerCount line 139
  16. lemma OAI.Percolation.BenjaminiSchramm.restrictedLayerCount_dependsOn line 147
  17. lemma OAI.Percolation.BenjaminiSchramm.restrictedLayerCount_mono_edges line 161
  18. theorem OAI.Percolation.BenjaminiSchramm.layerCount_le_frontier_sum line 172
  19. theorem OAI.Percolation.BenjaminiSchramm.lowerFrontierCell_fractional_bound line 207