OAI/Combinatorics/Coboundary/Realization.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Finite labeled coset complexes, purity, growth, incidence bounds, and weighted expansion reduction.

  1. abbrev OAI.CoboundaryExpanders.CosetConstruction.Vertex line 30
  2. instance OAI.CoboundaryExpanders.CosetConstruction.vertexFintype line 32
  3. def OAI.CoboundaryExpanders.CosetConstruction.labelEquiv line 35
  4. def OAI.CoboundaryExpanders.CosetConstruction.vertex line 38
  5. theorem OAI.CoboundaryExpanders.CosetConstruction.vertex_surjective line 41
  6. theorem OAI.CoboundaryExpanders.CosetConstruction.vertex_type_eq line 47
  7. theorem OAI.CoboundaryExpanders.CosetConstruction.vertex_injective line 51
  8. theorem OAI.CoboundaryExpanders.CosetConstruction.vertex_eq_iff line 54
  9. def OAI.CoboundaryExpanders.CosetConstruction.chamber line 60
  10. theorem OAI.CoboundaryExpanders.CosetConstruction.mem_chamber line 63
  11. theorem OAI.CoboundaryExpanders.CosetConstruction.vertex_mem_chamber line 67
  12. theorem OAI.CoboundaryExpanders.CosetConstruction.card_chamber line 70
  13. def OAI.CoboundaryExpanders.CosetConstruction.complex line 75
  14. theorem OAI.CoboundaryExpanders.CosetConstruction.mem_faces line 91
  15. theorem OAI.CoboundaryExpanders.CosetConstruction.chamber_mem_facesOf line 95
  16. theorem OAI.CoboundaryExpanders.CosetConstruction.pure line 100
  17. abbrev OAI.CoboundaryExpanders.CosetConstruction.Walk line 106
  18. theorem OAI.CoboundaryExpanders.CosetConstruction.walk_of_common_chamber line 110
  19. theorem OAI.CoboundaryExpanders.CosetConstruction.walk_symm line 119
  20. theorem OAI.CoboundaryExpanders.CosetConstruction.walk_vertex_mul line 127
  21. theorem OAI.CoboundaryExpanders.CosetConstruction.connected line 156
  22. def OAI.CoboundaryExpanders.CosetConstruction.incidentInChamber line 174
  23. theorem OAI.CoboundaryExpanders.CosetConstruction.mem_incidentInChamber line 178
  24. theorem OAI.CoboundaryExpanders.CosetConstruction.card_incidentInChamber line 182
  25. theorem OAI.CoboundaryExpanders.CosetConstruction.incident_faces_subset line 189
  26. theorem OAI.CoboundaryExpanders.CosetConstruction.topDegree_le line 206
  27. theorem OAI.CoboundaryExpanders.CosetConstruction.vertexCount_eq_sum_index line 222
  28. theorem OAI.CoboundaryExpanders.CosetConstruction.vertexCount_mul line 228
  29. theorem OAI.CoboundaryExpanders.CosetConstruction.vertexCount_mul_lower line 242
  30. def OAI.CoboundaryExpanders.Construction.localBound line 260
  31. theorem OAI.CoboundaryExpanders.Construction.localBound_pos line 262
  32. def OAI.CoboundaryExpanders.Construction.finiteCosetComplex line 264
  33. def OAI.CoboundaryExpanders.Construction.finiteSkeleton line 268
  34. theorem OAI.CoboundaryExpanders.Construction.finiteCosetComplex_pure line 271
  35. theorem OAI.CoboundaryExpanders.Construction.finiteSkeleton_pure line 276
  36. theorem OAI.CoboundaryExpanders.Construction.finiteCosetComplex_degree line 280
  37. theorem OAI.CoboundaryExpanders.Construction.finiteSkeleton_degree line 288
  38. theorem OAI.CoboundaryExpanders.Construction.finiteCosetComplex_growth_bound line 297
  39. theorem OAI.CoboundaryExpanders.Construction.finiteSkeleton_growth line 304
  40. theorem OAI.CoboundaryExpanders.Construction.finiteSkeleton_vertex_faces_growth line 315
  41. theorem OAI.CoboundaryExpanders.Construction.constructed_pure_bounded_growing line 319
  42. theorem OAI.CoboundaryExpanders.Construction.finiteCosetComplex_connected line 335
  43. theorem OAI.CoboundaryExpanders.Construction.finiteSkeleton_connected line 340
  44. theorem OAI.CoboundaryExpanders.Construction.constructed_connected_pure_bounded_growing line 344
  45. theorem OAI.CoboundaryExpanders.Construction.finiteSkeleton_zero_cohomology line 356
  46. abbrev OAI.CoboundaryExpanders.Complex.Chain line 367
  47. def OAI.CoboundaryExpanders.Complex.chainBasis line 369
  48. theorem OAI.CoboundaryExpanders.Complex.chainBasis_apply line 373
  49. def OAI.CoboundaryExpanders.Complex.boundaryLinear line 377
  50. theorem OAI.CoboundaryExpanders.Complex.boundary_on_face line 380
  51. theorem OAI.CoboundaryExpanders.Complex.boundary_boundary line 392
  52. def OAI.CoboundaryExpanders.Complex.chainComplex line 403
  53. theorem OAI.CoboundaryExpanders.Complex.chainComplex_d line 408
  54. theorem OAI.CoboundaryExpanders.Complex.cocycles_eq_coboundaries_of_homology_isZero line 412
  55. instance OAI.CoboundaryExpanders.InfiniteChains.Complex.finiteFaceFintype line 437
  56. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.boundary_single_subfaces line 439
  57. lemma OAI.CoboundaryExpanders.CosetConstruction.labelled_face_image line 469
  58. lemma OAI.CoboundaryExpanders.CosetConstruction.labelled_mem_faces line 474
  59. def OAI.CoboundaryExpanders.CosetConstruction.typedFaceEquiv line 491
  60. lemma OAI.CoboundaryExpanders.CosetConstruction.typedFaceEquiv_subset line 509
  61. def OAI.CoboundaryExpanders.CosetConstruction.typedChainEquiv line 516
  62. lemma OAI.CoboundaryExpanders.CosetConstruction.typedChainEquiv_single line 520
  63. lemma OAI.CoboundaryExpanders.CosetConstruction.typedChainEquiv_boundary line 525
  64. def OAI.CoboundaryExpanders.CosetConstruction.typedChainIso line 545
  65. theorem OAI.CoboundaryExpanders.CosetConstruction.cocycles_eq_coboundaries_of_typed_homology line 556
  66. theorem OAI.CoboundaryExpanders.Construction.finiteCosetComplex_positive_cohomology line 568
  67. theorem OAI.CoboundaryExpanders.Complex.cofaceCount_le_topDegree line 586
  68. theorem OAI.CoboundaryExpanders.Complex.cofaceCount_pos_of_pure line 594
  69. theorem OAI.CoboundaryExpanders.Complex.skeleton_cocycles line 599
  70. theorem OAI.CoboundaryExpanders.Complex.skeleton_cosystolic_iff line 613
  71. theorem OAI.CoboundaryExpanders.Complex.ambient_cosystolic_of_skeleton line 631
  72. def OAI.CoboundaryExpanders.Construction.UniformCosystolic line 658
  73. theorem OAI.CoboundaryExpanders.Construction.finiteCosetComplex_coface_bounds line 666
  74. theorem OAI.CoboundaryExpanders.Construction.constructed_expansion_of_open_inputs line 680
  75. theorem OAI.CoboundaryExpanders.reduction_to_three_open_inputs line 717