OAI/Probability/UnimodularPercolation/Kernel/Covariance.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Covariance for bond percolation.

  1. theorem OAI.Percolation.edgeFieldEquiv_symm_edgeFieldEquiv line 18
  2. theorem OAI.Percolation.spliceStateEquiv_symm_spliceStateEquiv line 23
  3. theorem OAI.Percolation.spliceCodeEquiv_symm_spliceCodeEquiv line 30
  4. theorem OAI.Percolation.spliceTrace_aut_map_iff line 39
  5. theorem OAI.Percolation.boundedTraceCodes_aut_map_iff line 53
  6. theorem OAI.Percolation.finiteTraceCodes_aut_map_iff line 67
  7. def OAI.Percolation.finiteTraceCodesEquiv line 77
  8. def OAI.Percolation.finiteTraceIndexEquiv line 97
  9. theorem OAI.Percolation.FiniteTraceIndexEquiv.input line 117
  10. theorem OAI.Percolation.FiniteTraceIndexEquiv.code line 121
  11. theorem OAI.Percolation.FiniteTraceIndexEquiv.output line 125
  12. theorem OAI.Percolation.FiniteTraceIndexEquiv.mass line 135
  13. theorem OAI.Percolation.finiteForwardLoad_aut_map line 152
  14. theorem OAI.Percolation.finset_aut_eq_map line 177
  15. def OAI.Percolation.finiteFieldAutEquiv line 182
  16. theorem OAI.Percolation.finiteFieldSet_aut_map line 189
  17. theorem OAI.Percolation.finiteFieldWeight_aut_map line 196
  18. def OAI.Percolation.finiteFamilyEquiv line 203
  19. theorem OAI.Percolation.finiteFieldFamily_aut_map line 208
  20. theorem OAI.Percolation.finiteFamilyWeight_aut_map line 217
  21. theorem OAI.Percolation.restrictFiniteField_aut_map line 224
  22. theorem OAI.Percolation.finiteRootLoad_aut_map line 235
  23. def OAI.Percolation.finiteChoiceTraceIndexEquiv line 265
  24. theorem OAI.Percolation.FiniteChoiceTraceIndexEquiv.input line 285
  25. theorem OAI.Percolation.FiniteChoiceTraceIndexEquiv.output line 289
  26. theorem OAI.Percolation.FiniteChoiceTraceIndexEquiv.mass line 295
  27. theorem OAI.Percolation.finiteChoiceForwardLoad_aut_map line 311
  28. theorem OAI.Percolation.edgeField_subset_aut_iff line 342
  29. theorem OAI.Percolation.finiteSpliceDomain_aut_map_iff line 352
  30. theorem OAI.Percolation.oldRunVertices_map line 363
  31. theorem OAI.Percolation.oldRunWeight_map line 374
  32. def OAI.Percolation.finiteVertexEquiv line 384
  33. def OAI.Percolation.finiteRunEquiv line 387
  34. theorem OAI.Percolation.amplificationVertices_aut_map line 391
  35. theorem OAI.Percolation.LocalEndpointRule.mass_aut_map line 400
  36. theorem OAI.Percolation.LocalEndpointRule.amplificationWeight_aut_map line 406
  37. theorem OAI.Percolation.LocalEndpointRule.amplificationInputs_aut_map_iff line 415
  38. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_aut_map line 454
  39. theorem OAI.Percolation.mem_incidentSupport_aut_iff line 474
  40. theorem OAI.Percolation.finiteBall_aut_iff line 481
  41. theorem OAI.Percolation.localBondBall_aut_iff line 486
  42. def OAI.Percolation.LocalEndpointRule.amplificationRadius line 507
  43. def OAI.Percolation.LocalEndpointRule.amplificationBall line 510
  44. def OAI.Percolation.LocalEndpointRule.amplificationBonds line 513
  45. def OAI.Percolation.LocalEndpointRule.amplifiedMass line 518
  46. theorem OAI.Percolation.LocalEndpointRule.amplifiedMass_nonneg line 524
  47. theorem OAI.Percolation.LocalEndpointRule.amplifiedMass_support line 531
  48. theorem OAI.Percolation.LocalEndpointRule.amplifiedMass_local line 542
  49. theorem OAI.Percolation.LocalEndpointRule.amplifiedMass_aut_map line 551
  50. def OAI.Percolation.LocalEndpointRule.amplificationLoad line 568
  51. theorem OAI.Percolation.LocalEndpointRule.amplificationBonds_query line 597
  52. theorem OAI.Percolation.LocalEndpointRule.amplificationBonds_root line 607
  53. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_row line 615
  54. theorem OAI.Percolation.LocalEndpointRule.amplificationRow_local line 626
  55. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_mean_finite line 634
  56. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_second_moment_finite line 644
  57. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_second_moment_le line 672
  58. def OAI.Percolation.finitePathTest line 710
  59. theorem OAI.Percolation.finitePathTest_zero line 713
  60. theorem OAI.Percolation.finitePathTest_succ line 717
  61. theorem OAI.Percolation.finitePathTest_support line 723
  62. theorem OAI.Percolation.finitePathTest_total line 743
  63. theorem OAI.Percolation.LocalEndpointRule.kernel_range_support line 784
  64. theorem OAI.Percolation.LocalEndpointRule.orbitBinConnection_range_support line 792
  65. theorem OAI.Percolation.LocalEndpointRule.amplificationBall_column line 802
  66. theorem OAI.Percolation.LocalEndpointRule.amplificationPath_total line 820
  67. theorem OAI.Percolation.LocalEndpointRule.amplificationMarginal_mean_pathTest line 865
  68. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_mean line 901
  69. def OAI.Percolation.CappedLocalLoad.kernel line 937
  70. theorem OAI.Percolation.CappedLocalLoad.kernel_nonneg line 940
  71. theorem OAI.Percolation.exists_operator_of_scaled_matrix line 946
  72. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_scaled_kernel line 965
  73. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_exists_operator line 979
  74. theorem OAI.Percolation.CappedLocalLoad.truncate_kernel_le line 1035
  75. theorem OAI.Percolation.CappedLocalLoad.truncate_exists_operator line 1044
  76. theorem OAI.Percolation.LocalEndpointRule.normalize_mass_operator line 1069
  77. theorem OAI.Percolation.LocalEndpointRule.mass_operator_of_normalized line 1084
  78. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_norm_pos line 1115
  79. theorem OAI.Percolation.LocalEndpointRule.amplification_truncation_step line 1133