OAI/Probability/UnimodularPercolation/Deformation/Corridors.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Corridors for bond percolation.

  1. theorem OAI.Percolation.RawCorridor.edge_has_label line 19
  2. theorem OAI.Percolation.RawCorridor.image_retained line 26
  3. theorem OAI.Percolation.RawCorridor.retained_ncard line 32
  4. theorem OAI.Percolation.RawCorridor.support_subset_of_retained line 40
  5. theorem OAI.Percolation.RawCorridor.retained_subset_of_support line 49
  6. theorem OAI.Percolation.RawCorridor.support_iff_retained line 54
  7. theorem OAI.Percolation.RawCorridor.retained_incident_interior line 58
  8. theorem OAI.Percolation.RawCorridor.specified_disjoint_exterior line 82
  9. def OAI.Percolation.edgePattern line 101
  10. theorem OAI.Percolation.edgePattern_eq_restriction line 104
  11. theorem OAI.Percolation.measurableSet_edgePattern line 125
  12. theorem OAI.Percolation.edgePattern_probability line 131
  13. def OAI.Percolation.RawCorridor.calibrationEvent line 153
  14. theorem OAI.Percolation.RawCorridor.calibrationEvent_eq line 156
  15. theorem OAI.Percolation.RawCorridor.calibration_probability line 161
  16. theorem OAI.Percolation.RawCorridor.calibration_identity line 173
  17. theorem OAI.Percolation.path_internal_two_neighbors line 195
  18. theorem OAI.Percolation.pivotal_image_mem_edges line 221
  19. theorem OAI.Percolation.RawCorridor.counted_terminal_outside line 240
  20. theorem OAI.Percolation.measurable_inter_const line 275
  21. theorem OAI.Percolation.restriction_events_independent line 282
  22. theorem OAI.Percolation.RawCorridor.calibration_restriction line 318
  23. theorem OAI.Percolation.RawCorridor.calibration_independent line 330
  24. theorem OAI.Percolation.conn_union_attachment line 362
  25. def OAI.Percolation.RawCorridor.exterior line 381
  26. def OAI.Percolation.RawCorridor.attachment line 384
  27. theorem OAI.Percolation.RawCorridor.support_exterior_ports line 387
  28. theorem OAI.Percolation.RawCorridor.attachment_closed line 392
  29. theorem OAI.Percolation.RawCorridor.open_subset_exterior_retained line 403
  30. theorem OAI.Percolation.RawCorridor.connection_exterior_or_attachment line 413
  31. theorem OAI.Percolation.RawCorridor.attachment_outside line 420
  32. theorem OAI.Percolation.RawCorridor.counted_exterior_orientation line 431
  33. def OAI.Percolation.RawCorridor.exteriorOrientations line 492
  34. theorem OAI.Percolation.RawCorridor.measurableSet_exteriorOrientations line 495
  35. theorem OAI.Percolation.RawCorridor.counted_subset_calibration_exterior line 501
  36. theorem OAI.Percolation.RawCorridor.exterior_orientation_BK line 518
  37. theorem OAI.Percolation.RawCorridor.counted_weight_bound line 529
  38. abbrev OAI.Percolation.RawFrom line 566
  39. def OAI.Percolation.RawFrom.zeroEquiv line 571
  40. def OAI.Percolation.RawFrom.succEquiv line 577
  41. instance OAI.Percolation.RawFrom.finite line 588
  42. def OAI.Percolation.RawFrom.integral line 595
  43. theorem OAI.Percolation.RawFrom.integral_zero line 598
  44. theorem OAI.Percolation.RawFrom.integral_succ line 604
  45. theorem OAI.Percolation.finite_openSimpleGraph_neighbors line 619
  46. theorem OAI.Percolation.sum_step_decomposition line 637
  47. theorem OAI.Percolation.raw_integral_operator line 662
  48. def OAI.Percolation.RawCorridor.counted line 703
  49. theorem OAI.Percolation.RawCorridor.counted_iff line 707
  50. theorem OAI.Percolation.RawCorridor.counted_base_mem_walk line 714
  51. theorem OAI.Percolation.RawCorridor.counted_symm line 724
  52. theorem OAI.Percolation.RawCorridor.measurableSet_counted line 728
  53. theorem OAI.Percolation.finite_corridors_on_bases line 737
  54. theorem OAI.Percolation.finite_counted_corridors line 756
  55. def OAI.Percolation.corridorPenaltyTerm line 779
  56. def OAI.Percolation.corridorPenalty line 783
  57. theorem OAI.Percolation.corridorPenaltyTerm_nonneg line 787
  58. theorem OAI.Percolation.corridorPenalty_finite_support line 796
  59. theorem OAI.Percolation.corridorPenalty_summable line 804
  60. theorem OAI.Percolation.corridorPenalty_nonneg line 809
  61. theorem OAI.Percolation.corridorPenalty_symm line 814
  62. theorem OAI.Percolation.corridorPenalty_restrict line 822
  63. theorem OAI.Percolation.measurable_corridorPenaltyTerm line 836
  64. theorem OAI.Percolation.measurable_corridorPenalty line 841
  65. def OAI.Percolation.deformedConnection line 859
  66. def OAI.Percolation.deformedKernel line 864
  67. theorem OAI.Percolation.deformedConnection_nonneg line 868
  68. theorem OAI.Percolation.deformedConnection_le_one line 876
  69. theorem OAI.Percolation.deformedConnection_symm line 885
  70. theorem OAI.Percolation.deformedConnection_mono line 894
  71. theorem OAI.Percolation.measurable_deformedConnection line 907
  72. theorem OAI.Percolation.integrable_deformedConnection line 916
  73. theorem OAI.Percolation.corridorPenalty_diag line 936
  74. theorem OAI.Percolation.deformedConnection_diag line 951
  75. theorem OAI.Percolation.deformedConnection_zero line 957
  76. theorem OAI.Percolation.deformedConnection_full_zero line 963
  77. theorem OAI.Percolation.deformedConnection_change line 969
  78. theorem OAI.Percolation.deformedKernel_zero line 986
  79. theorem OAI.Percolation.raw_diagram_hasSum line 1006
  80. theorem OAI.Percolation.sandwich_selfAdjoint line 1042
  81. theorem OAI.Percolation.raw_two_diagrams_hasSum line 1057
  82. theorem OAI.Percolation.integrable_corridorPenaltyTerm line 1088
  83. theorem OAI.Percolation.integral_corridorPenaltyTerm line 1093
  84. theorem OAI.Percolation.integral_corridorPenaltyTerm_le line 1101
  85. theorem OAI.Percolation.corridorPenalty_integrable_bound line 1136
  86. theorem OAI.Percolation.deformedKernel_change_bound line 1190
  87. theorem OAI.Percolation.deformedKernel_nonneg line 1223