OAI/Probability/UnimodularPercolation/Subdivision/Coupling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Coupling percolation on a graph with percolation on its subdivision.

  1. def OAI.Percolation.halfBit line 20
  2. def OAI.Percolation.seriesOpen line 46
  3. def OAI.Percolation.subdivisionOpen line 48
  4. theorem OAI.Percolation.halfBit_fst line 51
  5. theorem OAI.Percolation.seriesOpen_of_two_incident line 55
  6. theorem OAI.Percolation.subdivision_open_adj_iff line 75
  7. theorem OAI.Percolation.conn_subdivision_iff line 91
  8. theorem OAI.Percolation.map_bool_and line 141
  9. theorem OAI.Percolation.measurable_seriesOpen line 174
  10. theorem OAI.Percolation.law_map_seriesOpen line 186
  11. theorem OAI.Percolation.measurable_subdivisionOpen line 209
  12. theorem OAI.Percolation.law_map_subdivisionOpen line 213
  13. theorem OAI.Percolation.twoPoint_subdivision line 219
  14. theorem OAI.Percolation.conn_subdivision_inr line 232
  15. theorem OAI.Percolation.finite_cluster_subdivision_iff line 247
  16. theorem OAI.Percolation.exists_infinite_cluster_subdivision_iff line 272
  17. theorem OAI.Percolation.infinite_cluster_probability_subdivision line 301
  18. def OAI.Percolation.squareParameter line 315
  19. theorem OAI.Percolation.pc_subdivision_sq line 333