OAI/Probability/UnimodularPercolation/Escape/Labels.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Labels for bond percolation.

  1. structure OAI.Percolation.EscapeLabel line 18
  2. def OAI.Percolation.EscapeLabel.reverse line 30
  3. theorem OAI.Percolation.EscapeLabel.reverse_reverse line 39
  4. def OAI.Percolation.EscapeLabel.reverseEquiv line 43
  5. def OAI.Percolation.EscapeLabel.mass line 49
  6. theorem OAI.Percolation.EscapeLabel.mass_nonneg line 52
  7. theorem OAI.Percolation.EscapeLabel.mass_reverse line 57
  8. def OAI.Percolation.EscapeLabel.reverseRootedEquiv line 64
  9. def OAI.Percolation.RootedLabelCode line 84
  10. instance OAI.Percolation.finite_rootedLabelCode line 93
  11. def OAI.Percolation.labelFromCode line 101
  12. def OAI.Percolation.labelToCode line 114
  13. def OAI.Percolation.rootedLabelEquiv line 124
  14. theorem OAI.Percolation.finite_rootedEscapeLabels line 141
  15. theorem OAI.Percolation.segmentAnchors_card_on_orbit line 158
  16. theorem OAI.Percolation.segmentAnchors_card_eq_indicator line 165
  17. def OAI.Percolation.segmentReturnMass line 175
  18. theorem OAI.Percolation.labelFromCode_mass line 180
  19. theorem OAI.Percolation.rooted_label_mass_sum line 193
  20. theorem OAI.Percolation.segmentReturnMass_operator line 254
  21. theorem OAI.Percolation.segmentReturnMass_aut line 265
  22. theorem OAI.Percolation.segmentReturnMass_on_orbit line 280
  23. def OAI.Percolation.escapeLabelProbability line 291
  24. theorem OAI.Percolation.rooted_label_probability_sum line 299
  25. theorem OAI.Percolation.escapeLabelProbability_reverse line 322
  26. theorem OAI.Percolation.isAut_refl line 336
  27. def OAI.Percolation.EscapeLabel.autMap line 343
  28. theorem OAI.Percolation.EscapeLabel.autMap_trans line 353
  29. theorem OAI.Percolation.EscapeLabel.autMap_refl line 361
  30. theorem OAI.Percolation.EscapeLabel.autMap_symm line 369
  31. def OAI.Percolation.EscapeLabel.autEquiv line 382
  32. def OAI.Percolation.EscapeLabel.autRootedEquiv line 389
  33. theorem OAI.Percolation.EscapeLabel.mass_autMap line 399
  34. theorem OAI.Percolation.walkKernel_lazy line 419
  35. theorem OAI.Percolation.positive_lazy_power_step line 428
  36. theorem OAI.Percolation.walkPower_orbit_return_lower line 439
  37. theorem OAI.Percolation.segmentReturnMass_uniform_lower line 486
  38. theorem OAI.Percolation.rooted_label_probability_hasSum line 517
  39. def OAI.Percolation.labelEndpointEquiv line 552
  40. def OAI.Percolation.labelAutPairEquiv line 560
  41. def OAI.Percolation.escapeLabelTransport line 571
  42. theorem OAI.Percolation.escapeLabelTransport_reverse line 574
  43. theorem OAI.Percolation.escapeLabelTransport_aut line 580
  44. theorem OAI.Percolation.finite_pair_label_sigma line 590
  45. theorem OAI.Percolation.escapeLabelTransport_row_sum line 596
  46. theorem OAI.Percolation.escapeLabelTransport_rowSummable line 609
  47. theorem OAI.Percolation.escapeLabelTransport_columnSummable line 619
  48. theorem OAI.Percolation.EscapeLabel.first_orbit line 637
  49. theorem OAI.Percolation.EscapeLabel.last_orbit line 642
  50. theorem OAI.Percolation.escapeLabelTransport_zero line 647
  51. theorem OAI.Percolation.rooted_label_weight_reversal line 661
  52. theorem OAI.Percolation.escapeLabelProbability_aut line 724
  53. theorem OAI.Percolation.rooted_escape_label_reversal line 734
  54. theorem OAI.Percolation.escapeLabelProbability_nonneg line 751
  55. theorem OAI.Percolation.exists_geodesic_length line 776
  56. theorem OAI.Percolation.geodesic_getVert_dist line 794
  57. def OAI.Percolation.HoldingWalk.append line 817
  58. def OAI.Percolation.HoldingWalk.ofWalk line 822
  59. theorem OAI.Percolation.HoldingWalk.mass_append line 826
  60. theorem OAI.Percolation.HoldingWalk.mass_ofWalk line 834
  61. theorem OAI.Percolation.HoldingWalk.ofWalk_vertices line 840
  62. theorem OAI.Percolation.HoldingWalk.append_vertices line 845
  63. def OAI.Percolation.geodesicSegment line 869
  64. theorem OAI.Percolation.geodesicSegment_adj line 873
  65. theorem OAI.Percolation.geodesicSegment_injective line 881
  66. theorem OAI.Percolation.geodesicSegment_diameter line 890
  67. theorem OAI.Percolation.segmentOrbit_adj line 912
  68. theorem OAI.Percolation.walkKernel_step line 918
  69. theorem OAI.Percolation.walkKernel_ofWalk_mass line 923
  70. theorem OAI.Percolation.raw_tail_twoPoint_expectation line 940
  71. theorem OAI.Percolation.raw_tail_potential_bound line 956
  72. theorem OAI.Percolation.finite_weighted_markov line 1001
  73. theorem OAI.Percolation.raw_tail_potential_failure line 1012
  74. theorem OAI.Percolation.finite_product_failure_union line 1041
  75. theorem OAI.Percolation.two_raw_tail_potential_failure line 1069
  76. theorem OAI.Percolation.logarithmic_tail_power line 1112
  77. theorem OAI.Percolation.exists_uniform_logarithmic_tail_cutoff line 1126
  78. def OAI.Percolation.HoldingWalk.position line 1163
  79. theorem OAI.Percolation.HoldingWalk.position_zero line 1170
  80. theorem OAI.Percolation.HoldingWalk.position_length line 1173
  81. theorem OAI.Percolation.HoldingWalk.position_mem_vertices line 1179
  82. theorem OAI.Percolation.HoldingWalk.mem_vertices_iff_position line 1186