OAI/Probability/BenjaminiSchramm/SubdivisionGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Percolation.BenjaminiSchramm.subdivision_open_adj_inl_inr line 16
2. theorem OAI.Percolation.BenjaminiSchramm.exists_subdivision_lift_walk line 24
3. theorem OAI.Percolation.BenjaminiSchramm.exists_subdivision_compress_walk line 45
4. theorem OAI.Percolation.BenjaminiSchramm.subdivision_open_distance line 81
5. theorem OAI.Percolation.BenjaminiSchramm.subdivision_ambient_distance line 109
6. theorem OAI.Percolation.BenjaminiSchramm.subdivision_cluster_ncard_bounds line 120
7. theorem OAI.Percolation.BenjaminiSchramm.conn_subdivision_inr_adj line 163
8. theorem OAI.Percolation.BenjaminiSchramm.subdivision_intrinsicRadiusEvent line 177
9. theorem OAI.Percolation.BenjaminiSchramm.subdivision_extrinsicRadiusEvent line 199
10. theorem OAI.Percolation.BenjaminiSchramm.subdivision_volumeEvent_lower line 227
11. theorem OAI.Percolation.BenjaminiSchramm.subdivision_volumeEvent_upper line 237