OAI/Probability/UnimodularPercolation/Transport/TrajectoryMass.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Trajectory Mass for bond percolation.

  1. def OAI.Percolation.finiteFieldIntegral line 18
  2. theorem OAI.Percolation.finiteFieldIntegral_nonneg line 21
  3. theorem OAI.Percolation.finiteFieldIntegral_sum line 25
  4. theorem OAI.Percolation.finiteFamilyIntegral_prod line 34
  5. def OAI.Percolation.oldPathWeight line 45
  6. theorem OAI.Percolation.oldPathWeight_nonneg line 49
  7. theorem OAI.Percolation.oldPathWeight_integral line 54
  8. theorem OAI.Percolation.oldPathWeight_support line 64
  9. def OAI.Percolation.oldRunConsEquiv line 90
  10. def OAI.Percolation.oldRunWeight line 98
  11. theorem OAI.Percolation.oldRunWeight_nonneg line 102
  12. theorem OAI.Percolation.sum_oldRunWeight_succ line 108
  13. theorem OAI.Percolation.sum_oldRunWeight_le line 118
  14. theorem OAI.Percolation.sum_oldRunWeight_eq line 133
  15. def OAI.Percolation.oldRunVertices line 144
  16. theorem OAI.Percolation.oldRunVertices_last line 148
  17. theorem OAI.Percolation.oldRunVertices_succ_of_le line 152
  18. theorem OAI.Percolation.oldPathWeight_oldRunVertices line 159
  19. def OAI.Percolation.finiteOldKernel line 203
  20. theorem OAI.Percolation.finiteOldKernel_nonneg line 207
  21. theorem OAI.Percolation.oldRunWeight_integral line 214
  22. theorem OAI.Percolation.independent_oldRun_success line 234
  23. theorem OAI.Percolation.independent_oldRun_success_le line 245
  24. theorem OAI.Percolation.sum_comp_le_sum_of_injective line 266
  25. theorem OAI.Percolation.finite_sum_group_weight line 274
  26. theorem OAI.Percolation.finite_choice_fiber_le line 286
  27. theorem OAI.Percolation.finite_weighted_code_mass_le line 316
  28. theorem OAI.Percolation.finiteInverseLoad_weighted_le line 343
  29. theorem OAI.Percolation.finiteInverseLoad_oldRun_le line 433
  30. abbrev OAI.Percolation.FiniteChoiceTraceIndex line 470
  31. def OAI.Percolation.choiceTraceInput line 474
  32. def OAI.Percolation.choiceTraceOutput line 479
  33. def OAI.Percolation.choiceTraceCode line 484
  34. def OAI.Percolation.choiceTraceMass line 489
  35. theorem OAI.Percolation.choiceTrace_injective line 495
  36. def OAI.Percolation.finiteChoiceForwardLoad line 512
  37. theorem OAI.Percolation.finiteChoiceForwardLoad_bounds line 519
  38. theorem OAI.Percolation.sum_traceIndexMass line 552
  39. theorem OAI.Percolation.finiteChoiceForwardLoad_mean line 575
  40. def OAI.Percolation.auxiliaryTupleWeight line 621
  41. theorem OAI.Percolation.auxiliaryTupleWeight_nonneg line 624
  42. def OAI.Percolation.endpointRootMass line 630
  43. theorem OAI.Percolation.endpointRootMass_nonneg line 635
  44. theorem OAI.Percolation.finiteRootLoad_eq_sum line 646
  45. theorem OAI.Percolation.endpointRootMass_le line 676
  46. theorem OAI.Percolation.sum_endpointRootMass line 693
  47. theorem OAI.Percolation.finite_near_pair_mass_le_cover line 718
  48. theorem OAI.Percolation.finite_near_pair_mass_le line 749
  49. theorem OAI.Percolation.finiteInverseLoad_subtype line 784
  50. theorem OAI.Percolation.endpointInverseLoad_le line 799
  51. theorem OAI.Percolation.SpliceTrace.head_hanging line 845
  52. theorem OAI.Percolation.SpliceTrace.head_hanging_cap line 851
  53. theorem OAI.Percolation.finite_near_hanging_mass_le line 862
  54. def OAI.Percolation.oldRunArrival line 918
  55. theorem OAI.Percolation.oldRunArrival_nonneg line 921
  56. theorem OAI.Percolation.oldRunArrival_zero line 929
  57. theorem OAI.Percolation.oldRunArrival_succ line 935
  58. theorem OAI.Percolation.sum_oldRunArrival_le line 953
  59. theorem OAI.Percolation.sum_oldRunArrival_on_le line 971
  60. theorem OAI.Percolation.noSwitch_arrival_le line 980
  61. theorem OAI.Percolation.RootTransport.real line 1007
  62. theorem OAI.Percolation.transported_column_le line 1022
  63. theorem OAI.Percolation.finite_trajectory_hit_le line 1057
  64. theorem OAI.Percolation.mem_reachBall_aut_iff line 1082
  65. def OAI.Percolation.transportCut line 1091
  66. theorem OAI.Percolation.transportCut_mono line 1094
  67. theorem OAI.Percolation.transportCut_aut line 1098
  68. theorem OAI.Percolation.exists_transportCut line 1103
  69. theorem OAI.Percolation.transported_column_of_row_bound line 1120
  70. theorem OAI.Percolation.trajectory_hit_tsum_le line 1167
  71. theorem OAI.Percolation.finiteFamilyIntegral_mul_const line 1187
  72. theorem OAI.Percolation.oldRunWeight_factor_ne_zero line 1193
  73. def OAI.Percolation.finiteTrajectoryMass line 1202
  74. def OAI.Percolation.finiteTrajectoryHit line 1208
  75. theorem OAI.Percolation.finiteTrajectoryMass_nonneg line 1214
  76. theorem OAI.Percolation.finiteTrajectoryHit_nonneg line 1226
  77. theorem OAI.Percolation.finiteTrajectoryHit_le_sum line 1238
  78. theorem OAI.Percolation.finiteTrajectoryMass_finite_sum_le line 1263
  79. theorem OAI.Percolation.finiteTrajectoryMass_row_bound line 1307