OAI/Probability/IsingPerceptron/ArraySynchronization.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Array Synchronization.

  1. def OAI.IsingPerceptron.arrayBlock line 18
  2. def OAI.IsingPerceptron.HasGhirlandaGuerra line 23
  3. def OAI.IsingPerceptron.negativeBlock line 34
  4. lemma OAI.IsingPerceptron.matrix_sum_le_of_offDiagonal line 37
  5. lemma OAI.IsingPerceptron.posSemidef_sum_nonneg line 55
  6. lemma OAI.IsingPerceptron.no_large_negative_block line 59
  7. lemma OAI.IsingPerceptron.measurableSet_negative_finite line 68
  8. lemma OAI.IsingPerceptron.mem_negativeBlock_succ line 76
  9. lemma OAI.IsingPerceptron.negativeBlock_two line 103
  10. lemma OAI.IsingPerceptron.negativeBlock_next_probability line 119
  11. lemma OAI.IsingPerceptron.gg_negative_probability_zero line 170
  12. theorem OAI.IsingPerceptron.gg_pair_nonnegative line 206
  13. lemma OAI.IsingPerceptron.polya_no_linear_cap line 225
  14. lemma OAI.IsingPerceptron.equal_probability_aedisjoint_cap line 295
  15. abbrev OAI.IsingPerceptron.RealArray line 308
  16. def OAI.IsingPerceptron.permuteArray line 310
  17. def OAI.IsingPerceptron.WeaklyExchangeable line 315
  18. lemma OAI.IsingPerceptron.swap_hasFiniteSupport line 320
  19. lemma OAI.IsingPerceptron.measurable_permuteArray line 327
  20. def OAI.IsingPerceptron.starSet line 333
  21. def OAI.IsingPerceptron.duplicateSet line 338
  22. lemma OAI.IsingPerceptron.measurableSet_starSet line 344
  23. lemma OAI.IsingPerceptron.measurableSet_duplicateSet line 359
  24. lemma OAI.IsingPerceptron.starSet_permute line 372
  25. lemma OAI.IsingPerceptron.duplicateSet_permute line 395
  26. lemma OAI.IsingPerceptron.swap_preserves_ge line 410
  27. lemma OAI.IsingPerceptron.star_probability_equal line 418
  28. lemma OAI.IsingPerceptron.duplicate_probability_swap line 441
  29. lemma OAI.IsingPerceptron.duplicate_probability_equal line 456
  30. lemma OAI.IsingPerceptron.no_duplicate_star_cap line 474
  31. def OAI.IsingPerceptron.extendArrayBlock line 505
  32. lemma OAI.IsingPerceptron.measurable_extendArrayBlock line 508
  33. lemma OAI.IsingPerceptron.starSet_dependsOn line 520
  34. lemma OAI.IsingPerceptron.starSet_chain_succ line 545
  35. lemma OAI.IsingPerceptron.gg_star_chain_recurrence line 564
  36. lemma OAI.IsingPerceptron.low_pair_probability_equal line 620
  37. lemma OAI.IsingPerceptron.starSet_base line 631
  38. theorem OAI.IsingPerceptron.gg_duplication_positive line 645
  39. def OAI.IsingPerceptron.blockLaw line 671
  40. lemma OAI.IsingPerceptron.measurable_arrayBlock line 675
  41. lemma OAI.IsingPerceptron.blockLaw_support_compact line 681
  42. theorem OAI.IsingPerceptron.gg_duplicate_supported_last line 701
  43. lemma OAI.IsingPerceptron.support_mem_of_continuous_invariant line 793
  44. lemma OAI.IsingPerceptron.blockLaw_support_swap line 805
  45. lemma OAI.IsingPerceptron.isClosed_setOf_posSemidef line 832
  46. lemma OAI.IsingPerceptron.blockLaw_support_gram line 854
  47. lemma OAI.IsingPerceptron.real_posSemidef_symm line 873
  48. theorem OAI.IsingPerceptron.gg_duplicate_supported line 880
  49. lemma OAI.IsingPerceptron.psd_bilinear_symm line 954
  50. lemma OAI.IsingPerceptron.psd_cauchy_schwarz line 970
  51. lemma OAI.IsingPerceptron.psd_three_gap line 986
  52. def OAI.IsingPerceptron.groupAverageMatrix line 996
  53. lemma OAI.IsingPerceptron.groupAverageMatrix_posSemidef line 1000
  54. lemma OAI.IsingPerceptron.groupAverageMatrix_cross line 1018
  55. lemma OAI.IsingPerceptron.groupAverageMatrix_diag_le line 1025
  56. lemma OAI.IsingPerceptron.psd_entry_le_diagonal line 1050
  57. lemma OAI.IsingPerceptron.groupAverageMatrix_diag_le_common line 1058
  58. lemma OAI.IsingPerceptron.duplicated_triple_gap_bound line 1068
  59. lemma OAI.IsingPerceptron.no_arbitrary_nonultrametric_duplicates line 1105
  60. lemma OAI.IsingPerceptron.gg_duplicate_supported_of_two_le line 1122
  61. def OAI.IsingPerceptron.tripleLabel line 1140
  62. lemma OAI.IsingPerceptron.tripleLabel_castSucc line 1142
  63. lemma OAI.IsingPerceptron.gg_supported_populations line 1146
  64. lemma OAI.IsingPerceptron.gg_supported_triple_ordered line 1211
  65. lemma OAI.IsingPerceptron.array_entry_abs_le_diagonal line 1267
  66. lemma OAI.IsingPerceptron.gg_supported_triple_ultrametric line 1280
  67. theorem OAI.IsingPerceptron.gg_ultrametric_triple line 1304
  68. def OAI.IsingPerceptron.IsUltrametricArray line 1319
  69. lemma OAI.IsingPerceptron.ultrametric_survival_rectangle line 1322
  70. lemma OAI.IsingPerceptron.measurableSet_survival_compatible line 1335
  71. lemma OAI.IsingPerceptron.gg_survival_extension line 1340
  72. lemma OAI.IsingPerceptron.isCountablySpanning_real_Ici line 1364
  73. lemma OAI.IsingPerceptron.measure_eq_of_upper_orthants line 1372
  74. lemma OAI.IsingPerceptron.finite_permutation_extending line 1393
  75. lemma OAI.IsingPerceptron.gg_ultrametric line 1416
  76. lemma OAI.IsingPerceptron.blockLaw_measureReal_eq line 1453
  77. lemma OAI.IsingPerceptron.gg_survival_measure_eq line 1463
  78. lemma OAI.IsingPerceptron.gg_joint_extension_law line 1495
  79. def OAI.IsingPerceptron.augmentArrayBlock line 1542
  80. lemma OAI.IsingPerceptron.measurable_augmentArrayBlock line 1548
  81. lemma OAI.IsingPerceptron.augmentArrayBlock_eq line 1556
  82. lemma OAI.IsingPerceptron.gg_next_blockLaw_eq line 1572
  83. lemma OAI.IsingPerceptron.blockLaw_two_eq_pair_map line 1600
  84. lemma OAI.IsingPerceptron.blockLaw_restrict line 1617
  85. theorem OAI.IsingPerceptron.gg_blockLaw_unique line 1627
  86. lemma OAI.IsingPerceptron.HasEntryGhirlandaGuerra.map line 1653
  87. lemma OAI.IsingPerceptron.HasEntryGhirlandaGuerra.real_map line 1661
  88. lemma OAI.IsingPerceptron.gg_two_links_positive line 1666
  89. lemma OAI.IsingPerceptron.ultrametric_no_crossing line 1679
  90. theorem OAI.IsingPerceptron.jointGG_support_ordered line 1708