OAI/Probability/UnimodularPercolation/Transport/EndpointKernels.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Endpoint Kernels for bond percolation.

  1. theorem OAI.Percolation.finite_trace_pair_separated_le line 19
  2. def OAI.Percolation.finiteChoiceSeparatedPairMass line 133
  3. def OAI.Percolation.finiteChoiceHit line 156
  4. theorem OAI.Percolation.finiteChoiceSeparatedPairMass_le line 163
  5. structure OAI.Percolation.LocalEndpointRule line 234
  6. theorem OAI.Percolation.LocalEndpointRule.outside_ball_zero line 252
  7. theorem OAI.Percolation.LocalEndpointRule.summable_mass line 258
  8. theorem OAI.Percolation.LocalEndpointRule.mass_le_one line 265
  9. theorem OAI.Percolation.LocalEndpointRule.measurable_mass line 271
  10. theorem OAI.Percolation.LocalEndpointRule.integrable_mass line 285
  11. def OAI.Percolation.LocalEndpointRule.kernel line 292
  12. theorem OAI.Percolation.LocalEndpointRule.kernel_nonneg line 295
  13. theorem OAI.Percolation.LocalEndpointRule.kernel_outside_ball_zero line 298
  14. theorem OAI.Percolation.LocalEndpointRule.summable_kernel line 302
  15. theorem OAI.Percolation.LocalEndpointRule.kernel_row_integral line 311
  16. theorem OAI.Percolation.LocalEndpointRule.kernel_row_le_one line 322
  17. theorem OAI.Percolation.LocalEndpointRule.outside_reverse_ball_zero line 352
  18. theorem OAI.Percolation.LocalEndpointRule.kernel_outside_reverse_ball_zero line 360
  19. theorem OAI.Percolation.LocalEndpointRule.summable_kernel_column line 364
  20. theorem OAI.Percolation.LocalEndpointRule.mass_zero_of_start_not_mem line 371
  21. theorem OAI.Percolation.LocalEndpointRule.mass_zero_of_end_not_mem line 376
  22. theorem OAI.Percolation.LocalEndpointRule.kernel_zero_of_start_not_mem line 381
  23. theorem OAI.Percolation.LocalEndpointRule.kernel_zero_of_end_not_mem line 385
  24. theorem OAI.Percolation.LocalEndpointRule.kernel_covariant line 391
  25. def OAI.Percolation.LocalEndpointRule.successProbability line 399
  26. theorem OAI.Percolation.LocalEndpointRule.successProbability_nonneg line 402
  27. theorem OAI.Percolation.LocalEndpointRule.successProbability_le_one line 405
  28. theorem OAI.Percolation.LocalEndpointRule.successProbability_covariant line 408
  29. theorem OAI.Percolation.LocalEndpointRule.successProbability_orbit line 415
  30. theorem OAI.Percolation.LocalEndpointRule.kernel_column_covariant line 420
  31. theorem OAI.Percolation.LocalEndpointRule.kernel_column_orbit line 442
  32. theorem OAI.Percolation.LocalEndpointRule.kernel_column_eq_success line 450
  33. theorem OAI.Percolation.LocalEndpointRule.kernel_column_le_success line 503
  34. theorem OAI.Percolation.LocalEndpointRule.kernel_row_le_success line 530
  35. def OAI.Percolation.LocalEndpointRule.normalizedKernel line 539
  36. theorem OAI.Percolation.LocalEndpointRule.exists_normalized_operator line 545
  37. def OAI.Percolation.finiteFieldEquiv line 603
  38. theorem OAI.Percolation.finiteFieldEquiv_apply line 626
  39. theorem OAI.Percolation.finiteFieldEquiv_image line 629
  40. theorem OAI.Percolation.finiteFieldWeight_eq_atom line 638
  41. theorem OAI.Percolation.integral_finite_local line 652
  42. theorem OAI.Percolation.LocalEndpointRule.kernel_finite_sum line 678
  43. theorem OAI.Percolation.LocalEndpointRule.continuous_kernel line 683
  44. theorem OAI.Percolation.LocalEndpointRule.continuous_successProbability line 691
  45. theorem OAI.Percolation.internalEdges_aut_preimage line 713
  46. theorem OAI.Percolation.cutExists_aut_preimage line 725
  47. theorem OAI.Percolation.contactSet_aut_preimage line 736
  48. theorem OAI.Percolation.openMarkedPivotal_pair_aut line 742
  49. theorem OAI.Percolation.pivotalDistance_aut_preimage line 752
  50. theorem OAI.Percolation.goodForScale_aut_pullback line 763
  51. theorem OAI.Percolation.goodForScale_aut_iff line 795
  52. theorem OAI.Percolation.measurable_finite_local line 817
  53. theorem OAI.Percolation.integrable_finite_local line 829
  54. def OAI.Percolation.CappedGoodness line 844
  55. theorem OAI.Percolation.cappedGoodness_local line 847
  56. theorem OAI.Percolation.cappedGoodness_aut_iff line 866
  57. theorem OAI.Percolation.incidentSupport_ball_mono line 876
  58. theorem OAI.Percolation.finite_local_of_subset line 885
  59. theorem OAI.Percolation.finite_prop_local_of_subset line 904
  60. structure OAI.Percolation.CappedLocalLoad line 913
  61. def OAI.Percolation.CappedLocalLoad.row line 927
  62. theorem OAI.Percolation.CappedLocalLoad.row_nonneg line 930
  63. theorem OAI.Percolation.CappedLocalLoad.outside_ball_zero line 933
  64. theorem OAI.Percolation.CappedLocalLoad.summable_mass line 939
  65. theorem OAI.Percolation.CappedLocalLoad.mass_le_row line 945
  66. theorem OAI.Percolation.CappedLocalLoad.row_locality line 950
  67. theorem OAI.Percolation.CappedLocalLoad.row_covariance line 955
  68. theorem OAI.Percolation.CappedLocalLoad.integrable_mass line 961
  69. theorem OAI.Percolation.CappedLocalLoad.integrable_row line 965
  70. theorem OAI.Percolation.CappedLocalLoad.integrable_sq_row line 969
  71. def OAI.Percolation.CappedLocalLoad.truncate line 975
  72. theorem OAI.Percolation.CappedLocalLoad.cap_of_row_ne_zero line 1022
  73. theorem OAI.Percolation.CappedLocalLoad.truncate_scaled_row line 1030
  74. theorem OAI.Percolation.CappedLocalLoad.truncate_mass_le line 1039
  75. theorem OAI.Percolation.CappedLocalLoad.truncate_pointwise_loss line 1049
  76. theorem OAI.Percolation.CappedLocalLoad.truncate_mean_loss line 1081
  77. theorem OAI.Percolation.CappedLocalLoad.truncate_success_lower line 1106
  78. def OAI.Percolation.amplificationVertices line 1130
  79. def OAI.Percolation.LocalEndpointRule.amplificationWeight line 1136
  80. theorem OAI.Percolation.LocalEndpointRule.amplificationWeight_eq line 1140
  81. theorem OAI.Percolation.LocalEndpointRule.amplificationWeight_nonneg line 1145
  82. theorem OAI.Percolation.LocalEndpointRule.amplificationWeight_row line 1151
  83. def OAI.Percolation.LocalEndpointRule.amplificationInputs line 1163
  84. theorem OAI.Percolation.LocalEndpointRule.mem_amplificationInputs line 1169
  85. theorem OAI.Percolation.LocalEndpointRule.amplificationInputs_subset line 1177
  86. theorem OAI.Percolation.LocalEndpointRule.amplificationInputs_chain line 1182
  87. theorem OAI.Percolation.LocalEndpointRule.amplificationTrace_support line 1197