OAI/Probability/UnimodularPercolation/Splicing/ReferenceLaws.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Reference Laws for bond percolation.

  1. def OAI.Percolation.jointOutput line 19
  2. def OAI.Percolation.jointRestored line 24
  3. theorem OAI.Percolation.finite_joint_mass_le line 30
  4. def OAI.Percolation.trajectoryUnion line 114
  5. theorem OAI.Percolation.mem_trajectoryUnion line 118
  6. theorem OAI.Percolation.trajectoryUnion_finite_cap line 134
  7. theorem OAI.Percolation.SpliceTrace.added_subset_trajectory line 151
  8. theorem OAI.Percolation.SpliceTrace.trajectory_hits line 172
  9. theorem OAI.Percolation.SpliceTrace.added_finite_cap line 184
  10. theorem OAI.Percolation.SpliceTrace.joint_restored_field_symm line 205
  11. theorem OAI.Percolation.SpliceTrace.joint_restored_root line 223
  12. theorem OAI.Percolation.SpliceTrace.joint_trajectory_hits line 245
  13. theorem OAI.Percolation.SpliceTrace.joint_restored_size line 266
  14. def OAI.Percolation.hangingSide line 313
  15. theorem OAI.Percolation.hangingSide_finite line 316
  16. theorem OAI.Percolation.mem_hangingSide_iff_pivotal line 319
  17. theorem OAI.Percolation.hangingSide_ncard_add_rank line 327
  18. def OAI.Percolation.smallSeparatingBonds line 336
  19. theorem OAI.Percolation.smallSeparatingBonds_card_le line 340
  20. def OAI.Percolation.smallHangingThrough line 363
  21. theorem OAI.Percolation.mem_smallHangingThrough line 367
  22. theorem OAI.Percolation.smallHangingThrough_card_le line 373
  23. theorem OAI.Percolation.hangingSide_laminar line 399
  24. def OAI.Percolation.graphNeighbors line 415
  25. theorem OAI.Percolation.graphNeighbors_card_le line 418
  26. def OAI.Percolation.nearHangingEndpoints line 429
  27. theorem OAI.Percolation.nearHangingEndpoints_card_le line 435
  28. theorem OAI.Percolation.mem_nearHangingEndpoints_of_not_separated line 462
  29. abbrev OAI.Percolation.FiniteField line 505
  30. def OAI.Percolation.finiteFieldSet line 507
  31. def OAI.Percolation.finiteFieldWeight line 509
  32. theorem OAI.Percolation.domainBits_finiteFieldSet line 512
  33. theorem OAI.Percolation.finiteFieldWeight_nonneg line 519
  34. theorem OAI.Percolation.sum_finiteFieldWeight line 522
  35. def OAI.Percolation.finiteFieldFamily line 530
  36. theorem OAI.Percolation.finiteFieldFamily_at line 533
  37. def OAI.Percolation.finiteFamilyWeight line 538
  38. theorem OAI.Percolation.finiteFamilyWeight_nonneg line 541
  39. theorem OAI.Percolation.sum_finiteFamilyWeight line 545
  40. theorem OAI.Percolation.prod_fieldFamilyWeight line 551
  41. abbrev OAI.Percolation.FiniteJointData line 558
  42. def OAI.Percolation.encodeFiniteJoint line 561
  43. theorem OAI.Percolation.finiteFieldSet_injective line 565
  44. theorem OAI.Percolation.finiteFieldFamily_injective line 569
  45. theorem OAI.Percolation.encodeFiniteJoint_injective line 576
  46. theorem OAI.Percolation.jointTupleWeight_encode line 583
  47. theorem OAI.Percolation.sum_jointTupleWeight_encode line 593
  48. def OAI.Percolation.finiteFamilyEvent line 614
  49. theorem OAI.Percolation.finiteFamilyEvent_nonneg line 619
  50. theorem OAI.Percolation.finiteFamilyEvent_le_one line 625
  51. def OAI.Percolation.finiteJointDomain line 632
  52. theorem OAI.Percolation.finiteJointDomain_event_factor line 635
  53. theorem OAI.Percolation.mem_finiteJointDomain_of_support line 669
  54. theorem OAI.Percolation.exchangeOn_subset line 695
  55. theorem OAI.Percolation.finite_separated_second_moment_le line 714
  56. theorem OAI.Percolation.exists_seeded_spliceTrace line 785
  57. theorem OAI.Percolation.existsUnique_seeded_spliceTrace line 848
  58. theorem OAI.Percolation.reachBall_triangle line 878
  59. theorem OAI.Percolation.capped_cluster_ball_of_mem line 892
  60. theorem OAI.Percolation.oldChain_local_support line 901
  61. theorem OAI.Percolation.SpliceTrace.masks_in_deterministic_ball line 939
  62. theorem OAI.Percolation.oldChain_query_support line 957
  63. def OAI.Percolation.uniformRank line 983
  64. theorem OAI.Percolation.uniformRank_val_of_lt_one line 986
  65. theorem OAI.Percolation.uniformRank_eq_iff line 992
  66. theorem OAI.Percolation.volume_uniformRank_fiber line 1002
  67. def OAI.Percolation.uniformContact line 1013
  68. theorem OAI.Percolation.uniformContact_mem line 1017
  69. theorem OAI.Percolation.uniformContact_eq_iff line 1021
  70. theorem OAI.Percolation.volume_uniformContact_fiber line 1031
  71. def OAI.Percolation.chooseContact line 1039
  72. theorem OAI.Percolation.chooseContact_mem line 1045
  73. theorem OAI.Percolation.chooseContact_congr line 1064
  74. def OAI.Percolation.replaySeedFiber line 1070
  75. theorem OAI.Percolation.replaySeedFiber_univ line 1079
  76. theorem OAI.Percolation.SpliceTrace.follows_iff_seedFiber line 1089
  77. def OAI.Percolation.finiteContactSeeds line 1127
  78. theorem OAI.Percolation.finiteContactSeeds_at line 1130
  79. theorem OAI.Percolation.SpliceTrace.seed_event_eq_pi line 1135
  80. theorem OAI.Percolation.SpliceTrace.volume_seedFiber line 1154
  81. theorem OAI.Percolation.SpliceTrace.seed_probability line 1185