OAI/Probability/UnimodularPercolation/Kernel/ContactTrace.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Contact Trace for bond percolation.

  1. theorem OAI.Percolation.enn_ncard_eq_tsum line 19
  2. def OAI.Percolation.indexedEdgeKernel line 30
  3. theorem OAI.Percolation.indexedEdgeKernel_eq_ncard line 33
  4. theorem OAI.Percolation.indexedEdgeKernel_symm line 42
  5. theorem OAI.Percolation.indexedEdgeKernel_row line 45
  6. theorem OAI.Percolation.indexedEdgeKernel_aut line 60
  7. theorem OAI.Percolation.contact_endpoints_unique line 84
  8. theorem OAI.Percolation.closedContactSet_finite line 95
  9. theorem OAI.Percolation.clusterPairKernel_edge line 101
  10. theorem OAI.Percolation.closedContactSet_aut line 160
  11. theorem OAI.Percolation.clusterContactCount_aut line 173
  12. theorem OAI.Percolation.fullLargeContact_aut line 180
  13. theorem OAI.Percolation.fullLargeContact_cluster_constant line 185
  14. theorem OAI.Percolation.fullLargeContact_distinct line 195
  15. def OAI.Percolation.contactSquareLarge line 214
  16. theorem OAI.Percolation.contactSquareLarge_reroot line 219
  17. theorem OAI.Percolation.contactSquareLarge_bound line 260
  18. theorem OAI.Percolation.critical_contact_square_bound_nat line 304
  19. theorem OAI.Percolation.distinct_cluster_disjoint_occurrence line 347
  20. theorem OAI.Percolation.distinct_cluster_two_point_bound line 359
  21. theorem OAI.Percolation.measurable_clusterPairKernel line 369
  22. theorem OAI.Percolation.clusterPairKernel_cluster_constant line 378
  23. theorem OAI.Percolation.clusterPairKernel_aut line 387
  24. theorem OAI.Percolation.clusterPairKernel_distinct_integral line 410
  25. theorem OAI.Percolation.clusterPairKernel_distinct_bound line 443
  26. theorem OAI.Percolation.clusterPairFunctional_square_diagram line 453
  27. def OAI.Percolation.contactSquareLargeReal line 495
  28. theorem OAI.Percolation.contactSquareLargeReal_eq_ceil line 500
  29. theorem OAI.Percolation.critical_contact_square_bound line 510
  30. def OAI.Percolation.ennMatrixCoeff line 549
  31. theorem OAI.Percolation.ennMatrixCoeff_mul line 552
  32. theorem OAI.Percolation.ennMatrixCoeff_symm line 561
  33. theorem OAI.Percolation.HasKernel.ennMatrixCoeff line 566
  34. theorem OAI.Percolation.HasKernel.positiveRealMatrix line 573
  35. theorem OAI.Percolation.square_kernel_diagram line 580
  36. theorem OAI.Percolation.enn_rootTrace line 596
  37. theorem OAI.Percolation.rootTrace_six_le_cube line 625
  38. theorem OAI.Percolation.clusterPairFunctional_twoPoint_square_bound line 642
  39. def OAI.Percolation.finiteClusterWeight line 682
  40. theorem OAI.Percolation.finiteClusterWeight_expand line 685
  41. theorem OAI.Percolation.finiteClusterWeight_expectation_le line 707
  42. def OAI.Percolation.finitePairKernel line 729
  43. theorem OAI.Percolation.finitePairKernel_nonneg line 733
  44. theorem OAI.Percolation.finitePairKernel_exterior line 737
  45. def OAI.Percolation.finiteSmallPairKernel line 754
  46. def OAI.Percolation.finiteSmallClusterSize line 758
  47. theorem OAI.Percolation.finiteSmallPairKernel_bound line 762
  48. theorem OAI.Percolation.small_count_le_power line 815
  49. theorem OAI.Percolation.finiteSmallClusterSize_moment_bound line 827
  50. theorem OAI.Percolation.finiteSmallPairKernel_moment_bound line 847
  51. theorem OAI.Percolation.clusterPairKernel_finite line 872
  52. theorem OAI.Percolation.ofReal_finitePairKernel line 890
  53. def OAI.Percolation.smallPairKernel line 901
  54. theorem OAI.Percolation.smallPairKernel_eq_finite line 905
  55. theorem OAI.Percolation.smallPairKernel_lintegral_le_of_finite line 948
  56. theorem OAI.Percolation.smallPairKernel_moment_bound line 991
  57. theorem OAI.Percolation.matrixCoeff_positive_trace_norm line 1025
  58. theorem OAI.Percolation.smallPairKernel_twoPoint_bound line 1042
  59. theorem OAI.Percolation.measurable_smallPairKernel line 1087
  60. theorem OAI.Percolation.smallPairKernel_cluster_constant line 1094
  61. theorem OAI.Percolation.smallPairKernel_aut line 1104
  62. theorem OAI.Percolation.smallPairKernel_distinct line 1111
  63. theorem OAI.Percolation.contact_smallPairKernel_bound line 1119
  64. def OAI.Percolation.clusterPairMeasure line 1169
  65. theorem OAI.Percolation.clusterPairFunctional_eq_lintegral line 1175
  66. theorem OAI.Percolation.clusterPairFunctional_cauchy_schwarz line 1214