OAI/Probability/UnimodularPercolation/Escape/PathSelection.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Selection of geometrically separated paths from labelled escape events.

  1. theorem OAI.Percolation.HoldingWalk.mem_vertices_append line 21
  2. theorem OAI.Percolation.HoldingWalk.mem_vertices_fromPositions line 32
  3. def OAI.Percolation.negativeStem line 45
  4. theorem OAI.Percolation.positiveStem_vertices line 51
  5. theorem OAI.Percolation.negativeStem_vertices line 56
  6. def OAI.Percolation.labelLeftEscape line 66
  7. def OAI.Percolation.labelCorridor line 74
  8. def OAI.Percolation.segmentPositiveIndex line 79
  9. def OAI.Percolation.segmentNegativeIndex line 81
  10. theorem OAI.Percolation.segmentOrbit_injective line 84
  11. theorem OAI.Percolation.labelLeftEscape_raw_intersection line 91
  12. theorem OAI.Percolation.labelRaw_reverse_vertices line 130
  13. theorem OAI.Percolation.RawCorridor.interior_mem_raw line 143
  14. def OAI.Percolation.RawCorridor.neighborhood line 149
  15. theorem OAI.Percolation.RawCorridor.coe_neighborhood line 152
  16. def OAI.Percolation.RawCorridor.HasEscape line 157
  17. def OAI.Percolation.RawCorridor.Selected line 164
  18. def OAI.Percolation.spineVertices line 172
  19. def OAI.Percolation.spineNeighborhood line 179
  20. theorem OAI.Percolation.mem_spineVertices line 186
  21. theorem OAI.Percolation.labelCorridor_neighborhood_subset line 197
  22. theorem OAI.Percolation.neighborhood_card_le line 210
  23. theorem OAI.Percolation.spineVertices_card_le line 221
  24. theorem OAI.Percolation.spineNeighborhood_card_le line 240
  25. theorem OAI.Percolation.selected_of_good_label line 258
  26. theorem OAI.Percolation.rooted_selected_label_mass_lower line 318
  27. theorem OAI.Percolation.rootedEscapeLabelRaw_corridor line 397
  28. theorem OAI.Percolation.selected_raw_mass_of_label_mass line 409
  29. theorem OAI.Percolation.exists_full_selection_cutoffs line 433
  30. theorem OAI.Percolation.exists_selected_path_mass line 464