OAI/Probability/UnimodularPercolation/Splicing/MomentBounds.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Moment Bounds for bond percolation.

  1. theorem OAI.Percolation.uniformRank_fiber_eq line 19
  2. theorem OAI.Percolation.measurableSet_contactInterval line 39
  3. theorem OAI.Percolation.measurableSet_uniformRank_fiber line 43
  4. theorem OAI.Percolation.measurableSet_uniformContact_fiber line 51
  5. theorem OAI.Percolation.measurableSet_chooseContact_fiber line 63
  6. theorem OAI.Percolation.measurableSet_replaySeedFiber line 71
  7. theorem OAI.Percolation.SpliceTrace.measurableSet_seed_event line 83
  8. theorem OAI.Percolation.finite_bounded_lists line 103
  9. def OAI.Percolation.boundedTraceCodes line 113
  10. theorem OAI.Percolation.mem_boundedTraceCodes line 116
  11. theorem OAI.Percolation.SpliceTrace.length_le line 120
  12. theorem OAI.Percolation.SpliceTrace.mem_boundedTraceCodes line 127
  13. def OAI.Percolation.finiteTraceCodes line 139
  14. theorem OAI.Percolation.mem_finiteTraceCodes_iff line 144
  15. theorem OAI.Percolation.finite_trace_seed_partition line 152
  16. theorem OAI.Percolation.sum_finite_trace_probabilities line 184
  17. theorem OAI.Percolation.SpliceTrace.runMasks_execution line 225
  18. abbrev OAI.Percolation.FiniteSpliceData line 258
  19. def OAI.Percolation.encodeFiniteSplice line 261
  20. theorem OAI.Percolation.encodeFiniteSplice_injective line 265
  21. def OAI.Percolation.finiteSpliceDomain line 271
  22. theorem OAI.Percolation.spliceTupleWeight_encode line 274
  23. theorem OAI.Percolation.sum_finiteSpliceDomain line 280
  24. theorem OAI.Percolation.mem_finiteSpliceDomain_iff line 287
  25. theorem OAI.Percolation.exchangeState_mem_finiteSpliceDomain line 315
  26. theorem OAI.Percolation.runMasks_mem_finiteSpliceDomain line 331
  27. def OAI.Percolation.finiteInverseLoad line 354
  28. theorem OAI.Percolation.finiteInverseLoad_nonneg line 358
  29. theorem OAI.Percolation.finiteInverseLoad_le line 369
  30. theorem OAI.Percolation.finiteInverseLoad_density line 405
  31. abbrev OAI.Percolation.FiniteTraceIndex line 441
  32. def OAI.Percolation.traceIndexInput line 445
  33. def OAI.Percolation.traceIndexCode line 449
  34. def OAI.Percolation.traceIndexOutput line 453
  35. theorem OAI.Percolation.traceIndex_valid line 458
  36. theorem OAI.Percolation.traceIndex_injective line 473
  37. theorem OAI.Percolation.traceIndexOutput_mem line 484
  38. def OAI.Percolation.traceIndexMass line 501
  39. def OAI.Percolation.finiteForwardLoad line 507
  40. theorem OAI.Percolation.finiteForwardLoad_bounds line 513
  41. theorem OAI.Percolation.finiteForwardLoad_mean line 537
  42. theorem OAI.Percolation.finite_event_mass_le line 592
  43. theorem OAI.Percolation.finite_separated_contact_second_moment_le line 608
  44. def OAI.Percolation.finiteRootLoad line 694
  45. theorem OAI.Percolation.finiteRootLoad_nonneg line 699
  46. theorem OAI.Percolation.finiteRootLoad_le line 707
  47. theorem OAI.Percolation.finiteRootLoad_mean line 720
  48. theorem OAI.Percolation.finiteRootLoad_second_moment line 731
  49. theorem OAI.Percolation.finiteForwardRootLoad_bounds line 751
  50. theorem OAI.Percolation.finiteForwardRootLoad_mean line 767
  51. def OAI.Percolation.pairSpliceOutput line 793
  52. theorem OAI.Percolation.pairSpliceOutput_mem line 795
  53. theorem OAI.Percolation.finiteInverseLoad_mul line 804
  54. theorem OAI.Percolation.finiteRootLoad_pair_expansion line 829
  55. theorem OAI.Percolation.traceIndex_output_code_injective line 861
  56. theorem OAI.Percolation.jointRestored_injective line 890
  57. theorem OAI.Percolation.finite_joint_weighted_mass_le line 941
  58. def OAI.Percolation.finiteFamilyIntegral line 1002
  59. theorem OAI.Percolation.finiteFamilyIntegral_nonneg line 1006
  60. theorem OAI.Percolation.finiteFamilyIntegral_mono line 1010
  61. theorem OAI.Percolation.finiteFamilyIntegral_const line 1015
  62. theorem OAI.Percolation.finiteFamilyIntegral_sum line 1019
  63. theorem OAI.Percolation.finiteJointDomain_integral_factor line 1027
  64. theorem OAI.Percolation.finiteJointDomain_weighted_event_factor line 1047
  65. theorem OAI.Percolation.finite_separated_weighted_second_moment_le line 1088
  66. theorem OAI.Percolation.finite_separated_weighted_contact_second_moment_le line 1174