OAI/Combinatorics/Coboundary/Mixing.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Small-set expansion, local spectral descent, connectedness, and uniform coset mixing.

  1. def OAI.CoboundaryExpanders.EdgeMixing.volume line 23
  2. def OAI.CoboundaryExpanders.EdgeMixing.selected line 24
  3. def OAI.CoboundaryExpanders.EdgeMixing.chi line 25
  4. lemma OAI.CoboundaryExpanders.EdgeMixing.mean_chi line 27
  5. lemma OAI.CoboundaryExpanders.EdgeMixing.chi_sq line 34
  6. lemma OAI.CoboundaryExpanders.EdgeMixing.sum_right line 37
  7. lemma OAI.CoboundaryExpanders.EdgeMixing.centered_mean line 47
  8. lemma OAI.CoboundaryExpanders.EdgeMixing.centered_energy line 59
  9. lemma OAI.CoboundaryExpanders.EdgeMixing.centered_pairing line 75
  10. theorem OAI.CoboundaryExpanders.EdgeMixing.small_set line 98
  11. lemma OAI.CoboundaryExpanders.FatLadders.coface_eq_insert line 122
  12. lemma OAI.CoboundaryExpanders.FatLadders.sum_insert_star line 128
  13. def OAI.CoboundaryExpanders.FatLadders.linkEdge line 149
  14. lemma OAI.CoboundaryExpanders.FatLadders.linkEdge_nonneg line 153
  15. lemma OAI.CoboundaryExpanders.FatLadders.linkEdge_symm line 156
  16. lemma OAI.CoboundaryExpanders.FatLadders.linkEdge_mass line 160
  17. lemma OAI.CoboundaryExpanders.FatLadders.linkEdge_selected line 179
  18. lemma OAI.CoboundaryExpanders.FatLadders.linkEdge_volume line 193
  19. lemma OAI.CoboundaryExpanders.FatLadders.Collision.reconstruct line 207
  20. lemma OAI.CoboundaryExpanders.FatLadders.collision_le_pairing line 221
  21. theorem OAI.CoboundaryExpanders.FatLadders.localMixing_of_rayleigh line 268
  22. def OAI.CoboundaryExpanders.EdgeMixing.action line 331
  23. abbrev OAI.CoboundaryExpanders.EdgeMixing.Active line 332
  24. def OAI.CoboundaryExpanders.EdgeMixing.Connected line 333
  25. lemma OAI.CoboundaryExpanders.EdgeMixing.edge_le_mass line 336
  26. lemma OAI.CoboundaryExpanders.EdgeMixing.edge_zero_of_nonactive line 338
  27. def OAI.CoboundaryExpanders.EdgeMixing.activeEmbedding line 342
  28. def OAI.CoboundaryExpanders.EdgeMixing.activeGraph line 351
  29. lemma OAI.CoboundaryExpanders.EdgeMixing.active_action line 363
  30. theorem OAI.CoboundaryExpanders.EdgeMixing.trickle line 381
  31. lemma OAI.CoboundaryExpanders.EdgeMixing.energy_sub_const line 409
  32. lemma OAI.CoboundaryExpanders.EdgeMixing.pairing_sub_const line 415
  33. lemma OAI.CoboundaryExpanders.EdgeMixing.centered_bound line 440
  34. lemma OAI.CoboundaryExpanders.EdgeMixing.mass_mul_action line 451
  35. theorem OAI.CoboundaryExpanders.EdgeMixing.triangle_moment line 458
  36. theorem OAI.CoboundaryExpanders.EdgeMixing.triangle_trickle line 502
  37. def OAI.CoboundaryExpanders.FatLadders.triangle line 518
  38. lemma OAI.CoboundaryExpanders.FatLadders.triangle_cycle line 521
  39. lemma OAI.CoboundaryExpanders.FatLadders.triangle_symm line 527
  40. lemma OAI.CoboundaryExpanders.FatLadders.triangle_mass line 531
  41. lemma OAI.CoboundaryExpanders.FatLadders.triangle_sum line 545
  42. lemma OAI.CoboundaryExpanders.FatLadders.linkEdge_zero line 550
  43. theorem OAI.CoboundaryExpanders.FatLadders.link_trickle line 558
  44. theorem OAI.CoboundaryExpanders.FatLadders.link_trickle_double line 582
  45. theorem OAI.CoboundaryExpanders.FatLadders.all_link_rayleigh line 592
  46. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_chamberWeight line 624
  47. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_balanced line 635
  48. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.linkEdge_eq line 641
  49. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.active_face line 670
  50. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.edge_pos line 677
  51. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.VertexPath.toActive line 682
  52. theorem OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.spectralConnected line 697
  53. lemma OAI.CoboundaryExpanders.TypedCosetFaces.spectralConnected_of_generate line 709
  54. def OAI.CoboundaryExpanders.Construction.cycleGenerated line 722
  55. theorem OAI.CoboundaryExpanders.Construction.cycleRoot_mem_generated line 726
  56. theorem OAI.CoboundaryExpanders.Construction.cycleGenerated_le_U line 730
  57. theorem OAI.CoboundaryExpanders.Construction.upper_adjacent_mem_generated line 736
  58. theorem OAI.CoboundaryExpanders.Construction.upper_one_mem_generated line 747
  59. theorem OAI.CoboundaryExpanders.Construction.lower_X_mem_generated line 752
  60. theorem OAI.CoboundaryExpanders.Construction.X_mem_generated line 776
  61. theorem OAI.CoboundaryExpanders.Construction.X_pow_mem_generated line 813
  62. theorem OAI.CoboundaryExpanders.Construction.scalar_root_mem line 822
  63. theorem OAI.CoboundaryExpanders.Construction.upper_polynomial_mem_generated line 832
  64. theorem OAI.CoboundaryExpanders.Construction.X_polynomial_mem_generated line 846
  65. def OAI.CoboundaryExpanders.Construction.residue line 865
  66. theorem OAI.CoboundaryExpanders.Construction.residue_mk line 874
  67. theorem OAI.CoboundaryExpanders.Construction.residue_one_isUnit line 877
  68. theorem OAI.CoboundaryExpanders.Construction.map_E line 892
  69. def OAI.CoboundaryExpanders.Construction.truncatedIwahori line 897
  70. theorem OAI.CoboundaryExpanders.Construction.truncatedIwahori_entries line 901
  71. theorem OAI.CoboundaryExpanders.Construction.reduction_mem_truncatedIwahori line 909
  72. def OAI.CoboundaryExpanders.Construction.reducedGenerated line 918
  73. theorem OAI.CoboundaryExpanders.Construction.reducedGenerated_le line 921
  74. theorem OAI.CoboundaryExpanders.Construction.reducedGenerated_roots line 926
  75. theorem OAI.CoboundaryExpanders.Construction.truncatedIwahori_eq_generated line 940
  76. theorem OAI.CoboundaryExpanders.Construction.quotient_locals_generate line 949
  77. lemma OAI.CoboundaryExpanders.sqrt_div_le_of_sq line 988
  78. theorem OAI.CoboundaryExpanders.exists_spectral_threshold line 1001
  79. instance OAI.CoboundaryExpanders.TypedCosetFaces.vertexFintype line 1020
  80. lemma OAI.CoboundaryExpanders.TypedCosetFaces.finite_pure line 1022
  81. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.linkEdge_empty line 1037
  82. lemma OAI.CoboundaryExpanders.InfiniteChains.TopSpectral.changeFintype line 1042
  83. theorem OAI.CoboundaryExpanders.InfiniteChains.mixing_of_top_cones line 1048
  84. lemma OAI.CoboundaryExpanders.TypedCosetFaces.coset_mixing line 1074
  85. lemma OAI.CoboundaryExpanders.Construction.actual_mixing_level line 1088
  86. lemma OAI.CoboundaryExpanders.Construction.actual_mixing_mono line 1102
  87. theorem OAI.CoboundaryExpanders.Construction.uniform_actual_mixing line 1115