OAI/Computability/BinPacking/Expanders/SpectralCut.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean line 20
  2. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.energy line 22
  3. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.correlation line 24
  4. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.averagingOperator line 27
  5. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.iterateOperator line 30
  6. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeProfile line 35
  7. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeDensity line 38
  8. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.markedStep line 41
  9. def OAI.BinPackingGames.Foundations.PCP.SpectralReturn.returnMass line 45
  10. structure OAI.BinPackingGames.Foundations.PCP.SpectralReturn.SpectralCertificate line 49
  11. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 60
  12. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_equiv line 64
  13. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_prod line 68
  14. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_const line 73
  15. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_add line 76
  16. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_sub line 80
  17. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_mul_left line 84
  18. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_mul_right line 88
  19. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_nonnegative line 92
  20. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_mono line 95
  21. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.energy_nonnegative line 98
  22. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.correlation_sq_le line 101
  23. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.energy_sub_const line 105
  24. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.correlation_sub_const line 114
  25. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_operator line 132
  26. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.operator_sub_const line 142
  27. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_iterate line 150
  28. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.iterate_sub_const line 156
  29. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.mean_markedStep line 163
  30. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 191
  31. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.iterate_energy_bound line 198
  32. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 213
  33. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.correlation_centered line 228
  34. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 242
  35. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 247
  36. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 255
  37. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 259
  38. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 267
  39. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 270
  40. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 276
  41. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 283
  42. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 292
  43. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.returnMass_le line 308
  44. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 318
  45. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.geometric_sum_le line 328
  46. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.sum_returnMass_le line 341
  47. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 361
  48. theorem OAI.BinPackingGames.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 379
  49. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.zeroFrequency line 406
  50. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 408
  51. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cubeXor_assoc line 413
  52. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 419
  53. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.xorTranslation line 424
  54. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.rotate line 430
  55. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.rotate_involutive line 433
  56. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cayleyGraph line 438
  57. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 446
  58. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.splitPortWord line 449
  59. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.powerGenerators line 457
  60. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 461
  61. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cayleyAverage line 473
  62. def OAI.BinPackingGames.Foundations.PCP.CayleySpectral.eigenvalue line 476
  63. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 480
  64. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 483
  65. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 487
  66. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 508
  67. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 516
  68. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 533
  69. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.power_port_card line 558
  70. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.seven_power_port_card line 562
  71. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 566
  72. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 599
  73. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 610
  74. theorem OAI.BinPackingGames.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 621
  75. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.involutionEquiv line 639
  76. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 645
  77. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.squareFirst line 652
  78. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 656
  79. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.squareSwap line 662
  80. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 664
  81. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.square line 668
  82. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.square_rot_apply line 676
  83. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.square_next line 682
  84. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.cloudFirst line 685
  85. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 690
  86. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.crossCloud line 697
  87. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 700
  88. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.zigzag line 706
  89. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 714
  90. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 722
  91. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 725
  92. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 729
  93. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 732
  94. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 735
  95. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.cloudOperator line 740
  96. def OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.graphPermutation line 743
  97. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 746
  98. theorem OAI.BinPackingGames.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 755
  99. def OAI.BinPackingGames.Foundations.PCP.SpectralCut.indicator line 780
  100. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.mean_indicator line 782
  101. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.energy_indicator line 790
  102. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.indicator_nonnegative line 798
  103. def OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut line 805
  104. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut_density_eq line 812
  105. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut_density_ge_variance line 834
  106. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut_density_ge_quarter line 853
  107. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree line 869
  108. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.degree_mul_card_le_four_cut line 886
  109. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree_of_card_le_half line 895
  110. theorem OAI.BinPackingGames.Foundations.PCP.SpectralCut.cut_card_ge_twice line 902