OAI/Probability/UnimodularPercolation/Splicing/EndpointMoments.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Endpoint Moments for bond percolation.

  1. theorem OAI.Percolation.LocalEndpointRule.visitEnvelope_column_bound line 22
  2. theorem OAI.Percolation.LocalEndpointRule.finiteTrajectoryHit_sum_le line 42
  3. theorem OAI.Percolation.finiteChoiceHit_allRuns line 83
  4. def OAI.Percolation.allAmplificationVertices line 94
  5. def OAI.Percolation.LocalEndpointRule.allAmplificationWeight line 101
  6. def OAI.Percolation.LocalEndpointRule.allAmplificationInputs line 105
  7. theorem OAI.Percolation.LocalEndpointRule.allAmplificationWeight_nonneg line 110
  8. theorem OAI.Percolation.LocalEndpointRule.allAmplificationHit_bound line 117
  9. def OAI.Percolation.finiteClusterWindowMass line 149
  10. theorem OAI.Percolation.finiteChoiceHit_nonneg line 154
  11. theorem OAI.Percolation.LocalEndpointRule.amplificationSeparatedSecondMoment_le line 172
  12. theorem OAI.Percolation.finiteRootLoad_sum line 248
  13. theorem OAI.Percolation.finiteChoiceForwardLoad_prod line 257
  14. theorem OAI.Percolation.endpointRootMass_choice_prod line 270
  15. abbrev OAI.Percolation.LocalEndpointRule.AmplificationIndex line 297
  16. def OAI.Percolation.LocalEndpointRule.amplificationOutput line 302
  17. def OAI.Percolation.LocalEndpointRule.amplificationInput line 307
  18. def OAI.Percolation.LocalEndpointRule.amplificationCode line 312
  19. def OAI.Percolation.LocalEndpointRule.amplificationMass line 317
  20. def OAI.Percolation.LocalEndpointRule.amplificationRow line 322
  21. theorem OAI.Percolation.LocalEndpointRule.amplificationRow_eq_load line 326
  22. theorem OAI.Percolation.LocalEndpointRule.amplificationEndpointMass_eq line 344
  23. theorem OAI.Percolation.LocalEndpointRule.amplificationOutput_mem line 372
  24. theorem OAI.Percolation.LocalEndpointRule.amplificationMass_nonneg line 377
  25. theorem OAI.Percolation.LocalEndpointRule.amplificationIndex_trace line 383
  26. theorem OAI.Percolation.LocalEndpointRule.amplificationIndex_execution line 390
  27. theorem OAI.Percolation.LocalEndpointRule.amplificationIndex_support line 396
  28. theorem OAI.Percolation.LocalEndpointRule.amplificationIndex_caps line 404
  29. theorem OAI.Percolation.LocalEndpointRule.amplificationEndpointMass_outside line 412
  30. theorem OAI.Percolation.LocalEndpointRule.amplificationEndpointMass_bound line 425
  31. theorem OAI.Percolation.SpliceExecution.nil_iff line 452
  32. theorem OAI.Percolation.traceIndexMass_nil line 461
  33. theorem OAI.Percolation.finiteChoiceNilLoad_le line 470
  34. theorem OAI.Percolation.oldRunArrival_integral line 523
  35. def OAI.Percolation.LocalEndpointRule.amplificationNilRow line 539
  36. theorem OAI.Percolation.LocalEndpointRule.amplificationNilRow_arrival_le line 547
  37. theorem OAI.Percolation.LocalEndpointRule.amplificationNilRow_nonneg line 623
  38. theorem OAI.Percolation.LocalEndpointRule.amplificationNilRow_bound line 636
  39. def OAI.Percolation.LocalEndpointRule.amplificationAdded line 686
  40. def OAI.Percolation.LocalEndpointRule.amplificationNearPairMass line 690
  41. theorem OAI.Percolation.LocalEndpointRule.amplificationNearPairMass_bound line 702
  42. def OAI.Percolation.commonRootPairMass line 777
  43. theorem OAI.Percolation.finiteRootLoad_three_classes_le line 785
  44. theorem OAI.Percolation.finiteRootLoad_inverse_mean line 845
  45. theorem OAI.Percolation.LocalEndpointRule.amplificationRow_nonneg line 860
  46. theorem OAI.Percolation.LocalEndpointRule.amplificationRow_mean_eq line 868
  47. theorem OAI.Percolation.LocalEndpointRule.amplificationSeparated_class_eq line 879
  48. theorem OAI.Percolation.LocalEndpointRule.amplificationRow_second_moment_le line 927
  49. theorem OAI.Percolation.cluster_aut_preimage line 1016
  50. theorem OAI.Percolation.exchangeOn_preimage line 1022
  51. theorem OAI.Percolation.spliceMask_aut_preimage line 1026
  52. theorem OAI.Percolation.spliceField_aut_preimage line 1047
  53. theorem OAI.Percolation.seamContactCount_aut_preimage line 1054
  54. theorem OAI.Percolation.traceContactCount_aut_preimage line 1069
  55. def OAI.Percolation.edgeFieldEquiv line 1097
  56. def OAI.Percolation.spliceStateEquiv line 1103
  57. def OAI.Percolation.spliceCodeEquiv line 1106
  58. theorem OAI.Percolation.edgeFieldEquiv_apply line 1109
  59. theorem OAI.Percolation.spliceCodeEquiv_apply line 1112
  60. theorem OAI.Percolation.cluster_edgeFieldEquiv line 1115
  61. theorem OAI.Percolation.slitCluster_edgeFieldEquiv line 1121
  62. theorem OAI.Percolation.spliceStep_edgeFieldEquiv line 1130
  63. theorem OAI.Percolation.SpliceTrace.aut_map line 1144
  64. theorem OAI.Percolation.spliceStepMask_edgeFieldEquiv line 1181
  65. theorem OAI.Percolation.exchangeState_aut_map line 1192
  66. theorem OAI.Percolation.replaySplice_aut_map line 1208
  67. theorem OAI.Percolation.replayMasks_aut_map line 1222
  68. theorem OAI.Percolation.runMasks_aut_map line 1236
  69. theorem OAI.Percolation.seamContactCount_aut_map line 1246
  70. theorem OAI.Percolation.traceContactCount_aut_map line 1253