OAI/Probability/UnimodularPercolation/Splicing/Replay.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Replay for bond percolation.

  1. def OAI.Percolation.ValidSparseGapCode line 21
  2. def OAI.Percolation.sparseGapValue line 25
  3. theorem OAI.Percolation.sparseGapValue_zero line 29
  4. theorem OAI.Percolation.sparseGapValue_bound line 38
  5. theorem OAI.Percolation.sparseGapValue_injective line 50
  6. def OAI.Percolation.sparseGapArray line 121
  7. theorem OAI.Percolation.sparseGapArray_injective line 125
  8. theorem OAI.Percolation.SpliceTrace.valid_gap_code line 144
  9. def OAI.Percolation.seamContactCount line 192
  10. def OAI.Percolation.traceContactCount line 198
  11. theorem OAI.Percolation.SpliceTrace.contact_weight_bound line 205
  12. def OAI.Percolation.contactChoiceSet line 243
  13. theorem OAI.Percolation.volume_contactChoiceSet line 246
  14. theorem OAI.Percolation.real_volume_contact_choice_cube line 253
  15. theorem OAI.Percolation.SpliceTrace.contact_cube_le_code_weight line 265
  16. theorem OAI.Percolation.SpliceTrace.code_unique_of_gapCode line 284
  17. theorem OAI.Percolation.finite_inverse_contact_mass_le line 312
  18. def OAI.Percolation.GraphSeparated line 403
  19. theorem OAI.Percolation.GraphSeparated.symm line 406
  20. theorem OAI.Percolation.GraphSeparated.mono line 413
  21. theorem OAI.Percolation.GraphSeparated.no_shared_incidence line 417
  22. theorem OAI.Percolation.slit_cluster_remove_remote line 427
  23. theorem OAI.Percolation.spliceMask_remove_remote line 450
  24. theorem OAI.Percolation.spliceMask_incident line 465
  25. theorem OAI.Percolation.disjoint_spliceMasks line 475
  26. def OAI.Percolation.replaySplice line 498
  27. def OAI.Percolation.replayMasks line 506
  28. def OAI.Percolation.replayContacts line 515
  29. theorem OAI.Percolation.SpliceTrace.replay_eq line 523
  30. theorem OAI.Percolation.SpliceTrace.remote_replay line 532
  31. def OAI.Percolation.FollowsContactRule line 619
  32. theorem OAI.Percolation.followsContactRule_cons line 623
  33. theorem OAI.Percolation.SpliceTrace.remote_follows_contact_rule line 636
  34. theorem OAI.Percolation.SpliceTrace.seeded_unique line 649
  35. def OAI.Percolation.maskUnion line 693
  36. theorem OAI.Percolation.maskUnion_nil line 696
  37. theorem OAI.Percolation.maskUnion_cons line 700
  38. theorem OAI.Percolation.SpliceTrace.masks_incident line 706
  39. theorem OAI.Percolation.replaySplice_off_masks line 734
  40. theorem OAI.Percolation.SpliceTrace.masks_disjoint line 748
  41. theorem OAI.Percolation.conn_delete_rootBridge line 765
  42. theorem OAI.Percolation.cluster_double_cut line 782
  43. theorem OAI.Percolation.mask_not_crossing_remote line 804
  44. theorem OAI.Percolation.exchange_patch_symm line 816
  45. theorem OAI.Percolation.SpliceTrace.joint_root line 832
  46. def OAI.Percolation.runMasks line 927
  47. def OAI.Percolation.patchFirst line 932
  48. theorem OAI.Percolation.exchangeState_patchFirst line 935
  49. theorem OAI.Percolation.runMasks_patchFirst line 957
  50. theorem OAI.Percolation.SpliceTrace.runMasks_first line 970
  51. theorem OAI.Percolation.runMasks_weight line 998
  52. theorem OAI.Percolation.SpliceTrace.joint_replay_state line 1010
  53. theorem OAI.Percolation.SpliceTrace.endpoint_not_mem_of_ne_nil line 1049
  54. theorem OAI.Percolation.SpliceTrace.joint_virtual line 1058
  55. theorem OAI.Percolation.joint_restore_seeded_unique line 1106
  56. abbrev OAI.Percolation.JointSpliceState line 1172
  57. def OAI.Percolation.jointTupleWeight line 1174
  58. theorem OAI.Percolation.jointTupleWeight_nonneg line 1180
  59. theorem OAI.Percolation.replayMasks_indices line 1185
  60. theorem OAI.Percolation.replayMasks_indices_mem line 1194
  61. theorem OAI.Percolation.SpliceTrace.joint_weight line 1205