OAI/Combinatorics/Coboundary/LinkSpectrum.lean

GitHub source file

140 declarations, 0 contain sorry, 0 declared as axioms

Rank-two incidence geometry, weighted Rayleigh inequalities, and spectral bounds for links.

  1. def OAI.CoboundaryExpanders.RankTwoGeometry.matrix3 line 21
  2. lemma OAI.CoboundaryExpanders.RankTwoGeometry.matrix3_det line 22
  3. def OAI.CoboundaryExpanders.RankTwoGeometry.upper3 line 24
  4. def OAI.CoboundaryExpanders.RankTwoGeometry.ca line 30
  5. def OAI.CoboundaryExpanders.RankTwoGeometry.cb line 31
  6. def OAI.CoboundaryExpanders.RankTwoGeometry.cc line 32
  7. lemma OAI.CoboundaryExpanders.RankTwoGeometry.ca_upper3 line 34
  8. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cb_upper3 line 35
  9. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cc_upper3 line 36
  10. lemma OAI.CoboundaryExpanders.RankTwoGeometry.upper3_coords line 38
  11. lemma OAI.CoboundaryExpanders.RankTwoGeometry.upper_ext line 47
  12. lemma OAI.CoboundaryExpanders.RankTwoGeometry.upper3_mul line 51
  13. lemma OAI.CoboundaryExpanders.RankTwoGeometry.ca_mul line 59
  14. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cb_mul line 61
  15. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cc_mul line 63
  16. lemma OAI.CoboundaryExpanders.RankTwoGeometry.ca_one line 65
  17. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cb_one line 66
  18. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cc_one line 67
  19. lemma OAI.CoboundaryExpanders.RankTwoGeometry.ca_inv line 68
  20. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cb_inv line 72
  21. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cc_inv line 76
  22. def OAI.CoboundaryExpanders.RankTwoGeometry.pointCut line 81
  23. def OAI.CoboundaryExpanders.RankTwoGeometry.lineCut line 82
  24. lemma OAI.CoboundaryExpanders.RankTwoGeometry.mem_pointGroup line 83
  25. lemma OAI.CoboundaryExpanders.RankTwoGeometry.mem_lineGroup line 89
  26. lemma OAI.CoboundaryExpanders.RankTwoGeometry.point_rel line 96
  27. lemma OAI.CoboundaryExpanders.RankTwoGeometry.line_rel line 106
  28. abbrev OAI.CoboundaryExpanders.RankTwoGeometry.Vert line 126
  29. def OAI.CoboundaryExpanders.RankTwoGeometry.cosetVertex line 128
  30. lemma OAI.CoboundaryExpanders.RankTwoGeometry.point_vertex line 132
  31. lemma OAI.CoboundaryExpanders.RankTwoGeometry.line_vertex line 139
  32. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cuts3 line 148
  33. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cosetVertex_injective line 154
  34. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cosetVertex_surjective line 181
  35. def OAI.CoboundaryExpanders.RankTwoGeometry.vertexEquiv line 188
  36. def OAI.CoboundaryExpanders.RankTwoGeometry.incident line 191
  37. def OAI.CoboundaryExpanders.RankTwoGeometry.incidenceComplex line 193
  38. lemma OAI.CoboundaryExpanders.RankTwoGeometry.fullFace line 200
  39. lemma OAI.CoboundaryExpanders.RankTwoGeometry.face_subset_fullFace line 205
  40. lemma OAI.CoboundaryExpanders.RankTwoGeometry.cosetVertex_face_iff line 211
  41. def OAI.CoboundaryExpanders.RankTwoGeometry.incidenceModel line 235
  42. def OAI.CoboundaryExpanders.RankTwo.lineSum line 253
  43. def OAI.CoboundaryExpanders.RankTwo.pointSum line 254
  44. def OAI.CoboundaryExpanders.RankTwo.energy line 255
  45. def OAI.CoboundaryExpanders.RankTwo.pairing line 257
  46. lemma OAI.CoboundaryExpanders.RankTwo.energy_nonneg line 260
  47. lemma OAI.CoboundaryExpanders.RankTwo.affine_sum line 263
  48. lemma OAI.CoboundaryExpanders.RankTwo.adjoint line 272
  49. lemma OAI.CoboundaryExpanders.RankTwo.gram line 286
  50. lemma OAI.CoboundaryExpanders.RankTwo.gram_mean_zero line 300
  51. lemma OAI.CoboundaryExpanders.RankTwo.energy_eq_pairing line 309
  52. theorem OAI.CoboundaryExpanders.RankTwo.incidence_energy_identity line 312
  53. theorem OAI.CoboundaryExpanders.RankTwo.incidence_energy_bound line 325
  54. lemma OAI.CoboundaryExpanders.RankTwo.pairing_sq_le line 332
  55. theorem OAI.CoboundaryExpanders.RankTwo.incidence_pairing_bound line 337
  56. def OAI.CoboundaryExpanders.RankTwo.total line 342
  57. def OAI.CoboundaryExpanders.RankTwo.center line 344
  58. lemma OAI.CoboundaryExpanders.RankTwo.card_pos line 347
  59. lemma OAI.CoboundaryExpanders.RankTwo.total_center line 349
  60. lemma OAI.CoboundaryExpanders.RankTwo.energy_center line 356
  61. lemma OAI.CoboundaryExpanders.RankTwo.energy_center_le line 370
  62. lemma OAI.CoboundaryExpanders.RankTwo.total_lineSum line 374
  63. lemma OAI.CoboundaryExpanders.RankTwo.lineSum_center line 386
  64. lemma OAI.CoboundaryExpanders.RankTwo.incidence_center line 394
  65. theorem OAI.CoboundaryExpanders.RankTwo.opposition_rayleigh line 416
  66. def OAI.CoboundaryExpanders.EdgeMixing.mass line 454
  67. def OAI.CoboundaryExpanders.EdgeMixing.energy line 455
  68. def OAI.CoboundaryExpanders.EdgeMixing.pairing line 456
  69. def OAI.CoboundaryExpanders.EdgeMixing.Rayleigh line 457
  70. abbrev OAI.CoboundaryExpanders.RankTwo.Vert line 464
  71. def OAI.CoboundaryExpanders.RankTwo.edge line 465
  72. lemma OAI.CoboundaryExpanders.RankTwo.edge_symm line 471
  73. lemma OAI.CoboundaryExpanders.RankTwo.edge_nonneg line 474
  74. lemma OAI.CoboundaryExpanders.RankTwo.point_degree line 477
  75. lemma OAI.CoboundaryExpanders.RankTwo.line_degree line 484
  76. lemma OAI.CoboundaryExpanders.RankTwo.edge_degree line 488
  77. lemma OAI.CoboundaryExpanders.RankTwo.cross_pairing line 493
  78. lemma OAI.CoboundaryExpanders.RankTwo.edge_pairing line 509
  79. lemma OAI.CoboundaryExpanders.RankTwo.edge_energy line 535
  80. lemma OAI.CoboundaryExpanders.RankTwo.edge_mean line 541
  81. theorem OAI.CoboundaryExpanders.RankTwo.edge_rayleigh line 546
  82. lemma OAI.CoboundaryExpanders.EdgeMixing.sum_embedding line 561
  83. structure OAI.CoboundaryExpanders.EdgeMixing.Embedding line 570
  84. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.mass_map line 581
  85. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.mass_outside line 586
  86. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.mean_pull line 588
  87. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.energy_pull line 591
  88. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.pairing_pull line 595
  89. theorem OAI.CoboundaryExpanders.EdgeMixing.Embedding.push line 605
  90. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.level line 616
  91. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.mem_level line 621
  92. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces line 624
  93. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.Pure line 627
  94. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_zero_of_not_face line 630
  95. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_link line 639
  96. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.pure_link line 668
  97. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.cofaces_image line 694
  98. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.vertex_in_range line 718
  99. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.edge line 728
  100. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.edge_symm line 730
  101. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.edge_nonneg line 732
  102. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.edge_zero_of_not_face line 734
  103. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_pos line 741
  104. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_pos_iff line 745
  105. def OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.spectralEmbedding line 757
  106. theorem OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.rayleigh_push line 773
  107. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_top line 782
  108. lemma OAI.CoboundaryExpanders.RankTwoGeometry.point_line_face line 804
  109. lemma OAI.CoboundaryExpanders.RankTwoGeometry.point_point_not_face line 816
  110. lemma OAI.CoboundaryExpanders.RankTwoGeometry.line_line_not_face line 824
  111. lemma OAI.CoboundaryExpanders.RankTwoGeometry.incidence_edge line 832
  112. theorem OAI.CoboundaryExpanders.RankTwoGeometry.incidence_rayleigh line 856
  113. instance OAI.CoboundaryExpanders.MatrixOpposition.cutVertexFintype line 867
  114. theorem OAI.CoboundaryExpanders.MatrixOpposition.cut3_rayleigh line 869
  115. def OAI.CoboundaryExpanders.EdgeMixing.Embedding.extend line 882
  116. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.extend_map line 885
  117. lemma OAI.CoboundaryExpanders.EdgeMixing.Embedding.extend_comp line 891
  118. theorem OAI.CoboundaryExpanders.EdgeMixing.Embedding.pull line 893
  119. def OAI.CoboundaryExpanders.EdgeMixing.bipartiteEdge line 904
  120. lemma OAI.CoboundaryExpanders.EdgeMixing.bipartite_mass_left line 908
  121. lemma OAI.CoboundaryExpanders.EdgeMixing.bipartite_mass_right line 910
  122. lemma OAI.CoboundaryExpanders.EdgeMixing.bipartite_rayleigh line 913
  123. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.left_single_inl line 940
  124. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.right_single_inl line 942
  125. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.left_single_inr line 944
  126. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.right_single_inr line 946
  127. abbrev OAI.CoboundaryExpanders.InfiniteChains.Join.TrueVertex line 948
  128. def OAI.CoboundaryExpanders.InfiniteChains.Join.rankOneEmbedding line 950
  129. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.rankOne_rayleigh line 1011
  130. lemma OAI.CoboundaryExpanders.EdgeMixing.rayleigh_mono line 1018
  131. def OAI.CoboundaryExpanders.InfiniteChains.TopSpectral line 1030
  132. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.rayleigh_pull line 1034
  133. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.pushTopSpectral line 1039
  134. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.pullTopSpectral line 1045
  135. theorem OAI.CoboundaryExpanders.InfiniteChains.Join.topSpectral line 1052
  136. lemma OAI.CoboundaryExpanders.InfiniteChains.TopSpectral.vertexCriterion line 1072
  137. lemma OAI.CoboundaryExpanders.MatrixOpposition.cut_middle_topSpectral line 1102
  138. theorem OAI.CoboundaryExpanders.MatrixOpposition.cut_topSpectral line 1115
  139. lemma OAI.CoboundaryExpanders.TypedCosetFaces.allVertexTopSpectral_of_standard line 1161
  140. theorem OAI.CoboundaryExpanders.Construction.actual_topSpectral line 1183