OAI/Probability/UnimodularPercolation/Kernel/Amplification.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Amplification for bond percolation.

  1. def OAI.Percolation.restrictFiniteField line 18
  2. theorem OAI.Percolation.finiteFieldSet_restrict line 21
  3. theorem OAI.Percolation.restrictFiniteField_fieldSet line 26
  4. theorem OAI.Percolation.cluster_restrict_of_cap line 31
  5. def OAI.Percolation.LocalEndpointRule.amplificationMarginal line 54
  6. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_local line 60
  7. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_bounds line 69
  8. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_support line 82
  9. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_physical_support line 109
  10. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_mean line 121
  11. theorem OAI.Percolation.finiteSpliceDomain_integral_factor line 155
  12. def OAI.Percolation.finiteBinConnection line 171
  13. theorem OAI.Percolation.LocalEndpointRule.finiteOldKernel_eq_kernel line 178
  14. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_mean_kernel line 187
  15. def OAI.Percolation.binConnectionMass line 240
  16. theorem OAI.Percolation.binConnectionMass_nonneg line 244
  17. theorem OAI.Percolation.binConnectionMass_symm line 247
  18. theorem OAI.Percolation.binConnectionMass_local line 255
  19. theorem OAI.Percolation.binConnectionMass_support line 280
  20. theorem OAI.Percolation.binConnectionMass_outside line 288
  21. theorem OAI.Percolation.binConnectionMass_row line 294
  22. def OAI.Percolation.binConnection line 317
  23. theorem OAI.Percolation.binConnection_nonneg line 320
  24. theorem OAI.Percolation.binConnection_symm line 323
  25. theorem OAI.Percolation.binConnection_outside line 327
  26. theorem OAI.Percolation.binConnection_row line 331
  27. theorem OAI.Percolation.exists_binConnection_operator line 351
  28. theorem OAI.Percolation.finiteBinConnection_eq_binConnection line 379
  29. def OAI.Percolation.PositiveRealMatrix line 407
  30. theorem OAI.Percolation.PositiveRealMatrix.real line 413
  31. theorem OAI.Percolation.PositiveRealMatrix.mul_hasSum line 419
  32. theorem OAI.Percolation.PositiveRealMatrix.mul line 427
  33. theorem OAI.Percolation.PositiveRealMatrix.one line 438
  34. theorem OAI.Percolation.PositiveRealMatrix.pow line 443
  35. theorem OAI.Percolation.PositiveRealMatrix.star line 448
  36. theorem OAI.Percolation.oldRun_test_succ line 456
  37. theorem OAI.Percolation.finite_oldRun_operator_domination line 469
  38. theorem OAI.Percolation.isAut_trans line 503
  39. theorem OAI.Percolation.mem_vertexOrbit_aut_iff line 509
  40. theorem OAI.Percolation.binConnectionMass_covariant line 518
  41. theorem OAI.Percolation.binConnection_covariant line 528
  42. def OAI.Percolation.orbitBinConnection line 538
  43. theorem OAI.Percolation.orbitBinConnection_nonneg line 542
  44. theorem OAI.Percolation.orbitBinConnection_symm line 549
  45. theorem OAI.Percolation.orbitBinConnection_covariant line 553
  46. theorem OAI.Percolation.orbitBinConnection_summable line 558
  47. def OAI.Percolation.binOrbitRow line 565
  48. theorem OAI.Percolation.orbitBinConnection_row line 568
  49. theorem OAI.Percolation.orbitBinConnection_row_le line 575
  50. theorem OAI.Percolation.exists_orbitBinConnection_operator line 585
  51. theorem OAI.Percolation.oldRun_endpoint_mem line 609
  52. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_operator_le line 624
  53. theorem OAI.Percolation.exists_operator_of_amplification_domination line 668
  54. def OAI.Percolation.LocalEndpointRule.conditionalSuccess line 719
  55. theorem OAI.Percolation.LocalEndpointRule.conditionalSuccess_nonneg line 722
  56. theorem OAI.Percolation.LocalEndpointRule.conditionalSuccess_support line 725
  57. theorem OAI.Percolation.LocalEndpointRule.conditionalSuccess_local line 736
  58. theorem OAI.Percolation.LocalEndpointRule.conditionalSuccess_integrable line 741
  59. theorem OAI.Percolation.LocalEndpointRule.conditionalSuccess_mean line 745
  60. theorem OAI.Percolation.LocalEndpointRule.conditionalSuccess_covariant line 749
  61. def OAI.Percolation.LocalEndpointRule.clusterVisitMass line 758
  62. theorem OAI.Percolation.LocalEndpointRule.clusterVisitMass_nonneg line 761
  63. theorem OAI.Percolation.LocalEndpointRule.clusterVisitMass_outside line 768
  64. theorem OAI.Percolation.LocalEndpointRule.clusterVisitMass_local line 775
  65. theorem OAI.Percolation.LocalEndpointRule.clusterVisitMass_integrable line 796
  66. theorem OAI.Percolation.LocalEndpointRule.clusterVisitMass_covariant line 800
  67. theorem OAI.Percolation.LocalEndpointRule.clusterVisitMass_row_le line 811
  68. def OAI.Percolation.LocalEndpointRule.clusterVisitKernel line 826
  69. theorem OAI.Percolation.LocalEndpointRule.clusterVisitKernel_nonneg line 829
  70. theorem OAI.Percolation.LocalEndpointRule.clusterVisitKernel_outside line 832
  71. theorem OAI.Percolation.LocalEndpointRule.clusterVisitKernel_summable line 836
  72. theorem OAI.Percolation.LocalEndpointRule.clusterVisitKernel_row_le line 842
  73. theorem OAI.Percolation.LocalEndpointRule.clusterVisitKernel_covariant line 856
  74. def OAI.Percolation.LocalEndpointRule.visitEnvelope line 881
  75. theorem OAI.Percolation.LocalEndpointRule.visitEnvelope_nonneg line 887
  76. theorem OAI.Percolation.LocalEndpointRule.visitEnvelope_covariant line 895
  77. theorem OAI.Percolation.LocalEndpointRule.visitEnvelope_row_bound line 908
  78. theorem OAI.Percolation.oldRunWeight_congr line 967
  79. theorem OAI.Percolation.oldRunWeight_prod line 976
  80. def OAI.Percolation.markedOldRun line 997
  81. theorem OAI.Percolation.markedOldRun_nonneg line 1000
  82. theorem OAI.Percolation.markedOldRun_succ line 1011
  83. theorem OAI.Percolation.sum_markedOldRun_succ line 1028
  84. theorem OAI.Percolation.oldRunWeight_integral_indexed line 1038
  85. theorem OAI.Percolation.markedOldRun_integral line 1060
  86. theorem OAI.Percolation.trajectory_indicator_le_marked line 1079
  87. theorem OAI.Percolation.finiteTrajectoryMass_le_marked line 1128
  88. theorem OAI.Percolation.LocalEndpointRule.finite_marked_step_row_le line 1153
  89. theorem OAI.Percolation.LocalEndpointRule.sum_markedOldRun_le_envelope line 1174
  90. theorem OAI.Percolation.LocalEndpointRule.finiteTrajectoryMass_le_envelope line 1226