OAI/Probability/UnimodularPercolation/Kernel/RussoRows.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Russo Rows for bond percolation.

  1. theorem OAI.Percolation.clusterPairFunctional_mono_distinct line 19
  2. theorem OAI.Percolation.clusterPairFunctional_congr_ae line 38
  3. theorem OAI.Percolation.clusterPairFunctional_add line 57
  4. theorem OAI.Percolation.clusterPairKernel_symm line 74
  5. def OAI.Percolation.largeContactKernel line 97
  6. theorem OAI.Percolation.measurable_largeContactKernel line 102
  7. theorem OAI.Percolation.clusterPairFunctional_largeContact_sq line 110
  8. theorem OAI.Percolation.clusterPairFunctional_largeContact_bound line 124
  9. theorem OAI.Percolation.contact_smallTwoPoint_bound line 156
  10. theorem OAI.Percolation.contact_smallPairKernel_swap line 202
  11. theorem OAI.Percolation.clusterPairFunctional_twoPoint_mixed_bound line 222
  12. theorem OAI.Percolation.critical_mixed_trace_bound line 300
  13. theorem OAI.Percolation.closedPivotal_connection_iff line 360
  14. def OAI.Percolation.finiteClosedContact line 379
  15. theorem OAI.Percolation.finiteClosedContact_eq_sum line 384
  16. theorem OAI.Percolation.finite_connection_russo_contacts line 399
  17. theorem OAI.Percolation.finiteClosedContact_eq_full line 427
  18. theorem OAI.Percolation.finiteClosedContact_nonneg line 454
  19. theorem OAI.Percolation.finiteClosedContact_le_size line 459
  20. theorem OAI.Percolation.lower_cluster_restrict_eq line 476
  21. theorem OAI.Percolation.fullLargeContact_zero_le_size line 500
  22. theorem OAI.Percolation.integrable_fullContact_subcritical line 509
  23. theorem OAI.Percolation.fullContact_label_integral line 520
  24. theorem OAI.Percolation.fullContact_label_integrable line 528
  25. theorem OAI.Percolation.fullContact_eq_of_clusters line 536
  26. theorem OAI.Percolation.continuousAt_fullContact_expectation line 546
  27. def OAI.Percolation.ClusterSupportIn line 588
  28. theorem OAI.Percolation.measurableSet_clusterSupportIn line 591
  29. theorem OAI.Percolation.clusterSupportIn_of_incident line 611
  30. theorem OAI.Percolation.finiteClosedContact_eq_full_of_support line 617
  31. def OAI.Percolation.contactApproxError line 633
  32. theorem OAI.Percolation.measurable_contactApproxError line 638
  33. theorem OAI.Percolation.contactApproxError_nonneg line 645
  34. theorem OAI.Percolation.contactApproxError_le line 648
  35. theorem OAI.Percolation.contact_uniform_error_bound line 652
  36. theorem OAI.Percolation.integrable_contactApproxError line 682
  37. theorem OAI.Percolation.contactApproxError_integral_tendsto_zero line 690
  38. theorem OAI.Percolation.finiteClosedContact_label_integral line 710
  39. theorem OAI.Percolation.contactApproxError_label_integral line 718
  40. theorem OAI.Percolation.contact_expectation_uniform_error line 726
  41. def OAI.Percolation.realContactExpectation line 762
  42. theorem OAI.Percolation.realContactExpectation_coe line 765
  43. def OAI.Percolation.realTwoPoint line 769
  44. theorem OAI.Percolation.realTwoPoint_coe line 772
  45. theorem OAI.Percolation.finite_connection_deriv_eq line 776
  46. theorem OAI.Percolation.finite_connection_deriv_tendstoUniformlyOn line 784
  47. theorem OAI.Percolation.finite_connection_polynomial_tendsto_twoPoint line 810
  48. theorem OAI.Percolation.hasDerivAt_realTwoPoint_subcritical line 822
  49. def OAI.Percolation.russoDiagram line 855
  50. theorem OAI.Percolation.conn_probability_symm line 859
  51. theorem OAI.Percolation.conn_probability_mono line 865
  52. theorem OAI.Percolation.fullContact_lintegral_eq_kernel line 871
  53. theorem OAI.Percolation.fullContact_expectation_le_diagram line 883
  54. theorem OAI.Percolation.russoDiagram_mono line 892
  55. theorem OAI.Percolation.russoDiagram_symm line 898
  56. theorem OAI.Percolation.russoDiagram_row_bound line 906
  57. def OAI.Percolation.russoSlope line 945
  58. def OAI.Percolation.russoMajorant line 948
  59. theorem OAI.Percolation.russoDiagram_row_ne_top line 951
  60. theorem OAI.Percolation.russoDiagram_ne_top line 958
  61. theorem OAI.Percolation.summable_russoMajorant line 963
  62. theorem OAI.Percolation.russoSlope_nonneg line 968
  63. theorem OAI.Percolation.russoMajorant_nonneg line 972
  64. theorem OAI.Percolation.russoSlope_le_majorant line 975
  65. theorem OAI.Percolation.hasDerivAt_realTwoPoint_slope line 987
  66. theorem OAI.Percolation.russoMajorant_symm line 1007
  67. theorem OAI.Percolation.russoMajorant_uniform_row_bound line 1011
  68. theorem OAI.Percolation.summable_kernel_pair line 1027
  69. theorem OAI.Percolation.summable_twoPoint_pair line 1039
  70. theorem OAI.Percolation.summable_russoMajorant_pair line 1048
  71. def OAI.Percolation.realTriangleTerm line 1072
  72. def OAI.Percolation.realTriangleSlope line 1075
  73. def OAI.Percolation.triangleMajorant line 1080
  74. theorem OAI.Percolation.summable_triangleMajorant line 1085
  75. theorem OAI.Percolation.hasDerivAt_realTriangleTerm line 1093
  76. theorem OAI.Percolation.realTriangleSlope_nonneg line 1102
  77. theorem OAI.Percolation.realTriangleSlope_le_majorant line 1110
  78. def OAI.Percolation.realTriangle line 1147
  79. def OAI.Percolation.rootTriangle line 1150
  80. theorem OAI.Percolation.summable_realTriangleTerm line 1154
  81. theorem OAI.Percolation.summable_realTriangleSlope line 1165
  82. theorem OAI.Percolation.hasDerivAt_realTriangle_subcritical line 1175
  83. theorem OAI.Percolation.hasDerivAt_rootTriangle_subcritical line 1190