OAI/Probability/UnimodularPercolation/Splicing/GapCodes.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Gap Codes for bond percolation.

  1. abbrev OAI.Percolation.SpliceState line 21
  2. def OAI.Percolation.exchangeState line 25
  3. theorem OAI.Percolation.exchangeState_first line 28
  4. theorem OAI.Percolation.exchangeState_at line 31
  5. theorem OAI.Percolation.exchangeState_away line 35
  6. theorem OAI.Percolation.exchangeState_involutive line 39
  7. def OAI.Percolation.undoState line 54
  8. def OAI.Percolation.ValidSpliceStep line 59
  9. theorem OAI.Percolation.undoState_of_valid line 69
  10. inductive OAI.Percolation.SpliceExecution line 82
  11. def OAI.Percolation.undoExecution line 90
  12. theorem OAI.Percolation.SpliceExecution.undo line 95
  13. theorem OAI.Percolation.SpliceExecution.input_unique line 107
  14. theorem OAI.Percolation.SpliceTrace.realize line 115
  15. theorem OAI.Percolation.pivotal_mem_trail line 162
  16. theorem OAI.Percolation.finite_separatingBonds line 172
  17. def OAI.Percolation.separatingBonds line 186
  18. theorem OAI.Percolation.mem_separatingBonds line 189
  19. theorem OAI.Percolation.pivotalRank_injective_of_cluster_finite line 194
  20. def OAI.Percolation.bridgeIndex line 207
  21. theorem OAI.Percolation.bridgeIndex_pos line 210
  22. theorem OAI.Percolation.bridgeIndex_lt_of_rank_lt line 215
  23. theorem OAI.Percolation.bridgeIndex_injective line 232
  24. def OAI.Percolation.ordinalSpliceCode line 243
  25. theorem OAI.Percolation.ordinalSpliceCode_injective line 247
  26. theorem OAI.Percolation.SpliceTrace.input_unique_of_ordinalCode line 273
  27. def OAI.Percolation.domainBits line 304
  28. theorem OAI.Percolation.mem_domainBits line 306
  29. theorem OAI.Percolation.domainBits_subset line 309
  30. theorem OAI.Percolation.domainBits_exchange line 312
  31. def OAI.Percolation.spliceTupleWeight line 322
  32. theorem OAI.Percolation.spliceTupleWeight_nonneg line 327
  33. theorem OAI.Percolation.spliceTupleWeight_exchange line 333
  34. theorem OAI.Percolation.SpliceExecution.weight line 351
  35. theorem OAI.Percolation.splice_finite_weight_comparison line 365
  36. theorem OAI.Percolation.pivotalRank_lt_iff_of_cluster_finite line 403
  37. theorem OAI.Percolation.pivotal_internal_of_rank_lt line 434
  38. theorem OAI.Percolation.conn_far_end_avoids_later_pivotal line 446
  39. theorem OAI.Percolation.conn_near_end_avoids_earlier_pivotal line 460
  40. theorem OAI.Percolation.pivotal_between_is_internal line 475
  41. theorem OAI.Percolation.pivotal_after_is_internal line 503
  42. theorem OAI.Percolation.separatingBonds_card line 542
  43. def OAI.Percolation.bridgeInterval line 550
  44. theorem OAI.Percolation.bridgeIndex_interval_identity line 554
  45. theorem OAI.Percolation.bridgeInterval_card_le line 604
  46. theorem OAI.Percolation.bridge_gap_le_internal_distance line 623
  47. theorem OAI.Percolation.bridge_terminal_gap_le_internal_distance line 640
  48. theorem OAI.Percolation.pivotalDistance_le_cluster_card line 668
  49. theorem OAI.Percolation.inverse_contact_weight_le line 700
  50. theorem OAI.Percolation.conn_restrict_cluster_of_subset line 731
  51. theorem OAI.Percolation.conn_between_pivotals_internal line 744
  52. theorem OAI.Percolation.conn_after_pivotal_internal line 785
  53. theorem OAI.Percolation.pivotalDistance_le_induced_card line 801
  54. theorem OAI.Percolation.conn_after_pivotal_of_orientation line 823
  55. theorem OAI.Percolation.SpliceTrace.internal_agreement line 841
  56. theorem OAI.Percolation.SpliceTrace.head_cut line 865
  57. theorem OAI.Percolation.contactSet_finite line 879
  58. theorem OAI.Percolation.goodForScale_piece line 894
  59. theorem OAI.Percolation.slit_piece_connected line 910
  60. def OAI.Percolation.traceHeadGap line 934
  61. theorem OAI.Percolation.SpliceTrace.head_gap_bounds line 942
  62. theorem OAI.Percolation.SpliceTrace.seam_data line 1089
  63. theorem OAI.Percolation.SpliceTrace.head_index_lt line 1106
  64. def OAI.Percolation.gapSpliceCode line 1128
  65. def OAI.Percolation.decodeGapOrdinals line 1134
  66. theorem OAI.Percolation.SpliceTrace.decode_gap_code line 1141
  67. theorem OAI.Percolation.SpliceTrace.input_unique_of_gapCode line 1170
  68. def OAI.Percolation.gapWeight line 1200
  69. def OAI.Percolation.inverseCodeMass line 1203
  70. def OAI.Percolation.gapLetterWeight line 1207
  71. theorem OAI.Percolation.gapWeight_nonneg line 1209
  72. theorem OAI.Percolation.gapLetterWeight_nonneg line 1212
  73. theorem OAI.Percolation.sum_fin_succ_eq_Icc line 1218
  74. theorem OAI.Percolation.sum_gapLetterWeight line 1232
  75. theorem OAI.Percolation.total_gap_code_mass line 1241
  76. theorem OAI.Percolation.valid_gap_code_mass_le line 1248
  77. theorem OAI.Percolation.inverseCodeMass_le_harmonic line 1255
  78. theorem OAI.Percolation.inverseCodeMass_le_log line 1271
  79. def OAI.Percolation.contactInterval line 1284
  80. theorem OAI.Percolation.volume_contactInterval line 1287
  81. theorem OAI.Percolation.volume_contact_cube line 1308
  82. theorem OAI.Percolation.real_volume_contact_cube line 1315