OAI/Probability/UnimodularPercolation/Deformation/Calibration.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Calibration for bond percolation.

  1. theorem OAI.Percolation.exists_uniform_deformed_endpoint_comparison line 19
  2. theorem OAI.Percolation.pivotal_endpoint_connected line 60
  3. theorem OAI.Percolation.conn_delete_of_unconnected_endpoint line 68
  4. theorem OAI.Percolation.RawCorridor.retained_conn_base line 77
  5. theorem OAI.Percolation.RawCorridor.retained_conn line 84
  6. theorem OAI.Percolation.RawCorridor.retained_connects_support line 87
  7. theorem OAI.Percolation.RawCorridor.retained_nonempty line 91
  8. theorem OAI.Percolation.RawCorridor.counted_one_leg line 116
  9. theorem OAI.Percolation.RawCorridor.counted_split_legs line 171
  10. theorem OAI.Percolation.RawCorridor.counted_legs_of_disjoint line 199
  11. theorem OAI.Percolation.corridorPenaltyTerm_legs line 224
  12. theorem OAI.Percolation.corridorPenalty_legs line 257
  13. theorem OAI.Percolation.RawCorridor.base_not_interior line 292
  14. theorem OAI.Percolation.RawCorridor.endpoint_not_interior line 294
  15. theorem OAI.Percolation.deformedConnection_legs_lower line 299
  16. theorem OAI.Percolation.exists_uniform_corridor_leg_cost line 344
  17. theorem OAI.Percolation.simplePath_edge_cut line 379
  18. theorem OAI.Percolation.conn_closed_vertex_set line 420
  19. theorem OAI.Percolation.conn_edge_members line 439
  20. theorem OAI.Percolation.RawCorridor.calibration_pivotal_ports line 456
  21. theorem OAI.Percolation.RawCorridor.calibration_counted_of_orientation line 504
  22. theorem OAI.Percolation.RawCorridor.calibration_counted_iff line 533
  23. theorem OAI.Percolation.deformedConnection_restrict_config line 559
  24. def OAI.Percolation.exteriorLegProduct line 569
  25. theorem OAI.Percolation.exteriorLegProduct_nonneg line 575
  26. theorem OAI.Percolation.exteriorLegProduct_le_one line 585
  27. theorem OAI.Percolation.measurable_exteriorLegProduct line 598
  28. theorem OAI.Percolation.exteriorLegProduct_restrict line 608
  29. theorem OAI.Percolation.RawCorridor.measurableSet_calibration line 629
  30. theorem OAI.Percolation.RawCorridor.calibration_integral line 640
  31. theorem OAI.Percolation.RawCorridor.calibration_weighted_integral line 652
  32. theorem OAI.Percolation.calibrated_leg_product_le_term line 678
  33. theorem OAI.Percolation.integrable_corridorDerivativeTerm line 711
  34. theorem OAI.Percolation.integrable_exteriorLegProduct line 738
  35. theorem OAI.Percolation.calibrated_derivative_kernel_lower line 750
  36. theorem OAI.Percolation.real_tonelli_of_integrable_sum line 786
  37. theorem OAI.Percolation.exteriorLegProduct_sum line 820
  38. theorem OAI.Percolation.exteriorLegProduct_integral_sum line 846
  39. theorem OAI.Percolation.integral_corridorDerivativeTerm_le line 885
  40. theorem OAI.Percolation.summable_twoPoint_pairs line 899
  41. theorem OAI.Percolation.integral_corridorDerivativeTerm_nonneg line 909
  42. theorem OAI.Percolation.summable_corridorDerivativeTerm_pairs line 917
  43. theorem OAI.Percolation.calibrated_derivative_template_lower line 948
  44. theorem OAI.Percolation.calibrated_derivative_template_row_lower line 971
  45. theorem OAI.Percolation.walk_map_dropUntil line 1003
  46. theorem OAI.Percolation.walk_map_bypass line 1022
  47. def OAI.Percolation.HoldingWalk.map line 1039
  48. theorem OAI.Percolation.HoldingWalk.map_vertices line 1044
  49. theorem OAI.Percolation.HoldingWalk.map_withoutHolds line 1051
  50. theorem OAI.Percolation.HoldingWalk.map_erase line 1058
  51. theorem OAI.Percolation.HoldingWalk.map_map line 1077
  52. theorem OAI.Percolation.HoldingWalk.map_id line 1084
  53. theorem OAI.Percolation.HoldingWalk.mass_map line 1090
  54. def OAI.Percolation.rawWalkMap line 1099
  55. theorem OAI.Percolation.rawWalkMap_comp line 1102
  56. theorem OAI.Percolation.rawWalkMap_id line 1111
  57. def OAI.Percolation.rawWalkEquiv line 1120
  58. theorem OAI.Percolation.openSimpleGraph_univ_adj line 1142
  59. def OAI.Percolation.autSimpleGraph line 1146
  60. def OAI.Percolation.RawCorridor.autEquiv line 1157
  61. theorem OAI.Percolation.RawCorridor.aut_path line 1160
  62. theorem OAI.Percolation.RawCorridor.aut_path_length line 1164
  63. theorem OAI.Percolation.RawCorridor.aut_base line 1182
  64. theorem OAI.Percolation.RawCorridor.aut_endpoint line 1185
  65. theorem OAI.Percolation.RawCorridor.aut_support line 1188
  66. theorem OAI.Percolation.RawCorridor.aut_edges line 1193
  67. theorem OAI.Percolation.RawCorridor.aut_interior line 1198
  68. theorem OAI.Percolation.RawCorridor.aut_retained line 1205
  69. theorem OAI.Percolation.RawCorridor.aut_blockers line 1210
  70. theorem OAI.Percolation.RawCorridor.aut_blockers_ncard line 1225
  71. theorem OAI.Percolation.RawCorridor.aut_probability line 1233
  72. theorem OAI.Percolation.RawCorridor.aut_weight line 1238