OAI/Probability/UnimodularPercolation/Splicing/Geometry.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Critical parameters and the geometry, selection and traces of splices.

  1. theorem OAI.Percolation.twoPoint_adj_lower line 20
  2. theorem OAI.Percolation.walk_operator_apply line 33
  3. theorem OAI.Percolation.parameter_le_walk_norm line 47
  4. theorem OAI.Percolation.pc_lt_one_of_nonamenable line 86
  5. def OAI.Percolation.exchangeOn line 114
  6. theorem OAI.Percolation.mem_exchangeOn line 116
  7. theorem OAI.Percolation.exchangeOn_involutive line 120
  8. def OAI.Percolation.spliceMask line 127
  9. def OAI.Percolation.spliceField line 130
  10. theorem OAI.Percolation.slit_cluster_subset line 133
  11. theorem OAI.Percolation.spliceMask_not_internal line 137
  12. theorem OAI.Percolation.spliceMask_of_internal_piece line 144
  13. theorem OAI.Percolation.splice_internal_fields line 151
  14. theorem OAI.Percolation.splice_crossing_unique line 168
  15. theorem OAI.Percolation.splice_cluster line 184
  16. theorem OAI.Percolation.splice_seam_pivotal line 243
  17. theorem OAI.Percolation.splice_close_seam_cluster line 281
  18. theorem OAI.Percolation.splice_recover_piece line 313
  19. def OAI.Percolation.recoveredMask line 333
  20. theorem OAI.Percolation.recoveredMask_splice line 337
  21. def OAI.Percolation.undoSplice line 350
  22. theorem OAI.Percolation.undoSplice_of_valid line 355
  23. theorem OAI.Percolation.spliceMask_finite line 371
  24. def OAI.Percolation.finiteExchange line 383
  25. theorem OAI.Percolation.coe_finiteExchange line 385
  26. theorem OAI.Percolation.finiteExchange_card line 389
  27. theorem OAI.Percolation.finiteExchange_card_sum line 394
  28. theorem OAI.Percolation.finiteExchange_subset line 401
  29. theorem OAI.Percolation.bernoulliWeight_exchange line 409
  30. def OAI.Percolation.deletionContacts line 434
  31. def OAI.Percolation.DeletionGoodForScale line 439
  32. theorem OAI.Percolation.deleted_cluster_subset line 447
  33. theorem OAI.Percolation.contactSet_deleted_cluster line 454
  34. theorem OAI.Percolation.goodForScale_iff_deletion line 473
  35. theorem OAI.Percolation.capped_good_local line 524
  36. theorem OAI.Percolation.measurableSet_capped_good line 547
  37. theorem OAI.Percolation.exists_maximal_splice_index line 569
  38. theorem OAI.Percolation.exists_splice_contact line 607
  39. theorem OAI.Percolation.splice_cluster_cap line 616
  40. theorem OAI.Percolation.cluster_eq_of_incident_agreement line 637
  41. theorem OAI.Percolation.spliceMask_avoids_prefix line 657
  42. theorem OAI.Percolation.splice_preserves_prefix_cut line 671
  43. inductive OAI.Percolation.SpliceTrace line 689
  44. theorem OAI.Percolation.exists_spliceTrace line 706
  45. theorem OAI.Percolation.SpliceTrace.cluster_subset line 751
  46. theorem OAI.Percolation.SpliceTrace.preserve_cut line 763
  47. theorem OAI.Percolation.SpliceTrace.endpoint line 785
  48. theorem OAI.Percolation.SpliceTrace.seams_pivotal line 794