OAI/Combinatorics/Coboundary/Complex.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CoboundaryExpanders.Complex line 19

   Source documentation

   A finite abstract simplicial complex, including its empty face. Every labelled vertex is a vertex of the complex, so unused labels are disallowed.

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:19 (same declaration text).

   structure Complex where
   …

2. def OAI.CoboundaryExpanders.Complex.facesOf line 29

   Source documentation

   Faces of dimension i, i.e. with exactly i+1 vertices.

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:29 (same declaration text).

   def facesOf (X : Complex) (i : ℕ) : Finset (Finset (Fin X.vertexCount)) :=
   …

   Mentions: OAI.CoboundaryExpanders.Complex

3. def OAI.CoboundaryExpanders.Complex.Face line 32

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:32 (same declaration text).

4. instance OAI.CoboundaryExpanders.Complex.(instance at line 34) line 34
5. instance OAI.CoboundaryExpanders.Complex.(instance at line 35) line 35
6. def OAI.CoboundaryExpanders.Complex.Pure line 38

   Source documentation

   Nonempty top face set and every face contained in an s-face: exact purity.

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:38 (same declaration text).

   def Pure (X : Complex) (s : ℕ) : Prop :=
   …

   Mentions: OAI.CoboundaryExpanders.Complex

7. def OAI.CoboundaryExpanders.Complex.Connected line 43

   Source documentation

   Connectedness of the one-skeleton, including nonemptiness.

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:43 (same declaration text).

   def Connected (X : Complex) : Prop :=
   …

   Mentions: OAI.CoboundaryExpanders.Complex

8. abbrev OAI.CoboundaryExpanders.Complex.Cochain line 48

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:48 (same declaration text).

9. def OAI.CoboundaryExpanders.Complex.weight line 51

   Source documentation

   Source equation (weights), with ambient pure dimension s.

   Also declared: ComparatorChallenges/CoboundaryExpanders.lean:51 (same declaration text).

   def weight (X : Complex) (s i : ℕ) (σ : X.Face i) : ℝ :=
   …

   Mentions: OAI.CoboundaryExpanders.Complex

10. def OAI.CoboundaryExpanders.Complex.norm line 56

    Source documentation

    The source's weighted support norm, not the unweighted Hamming norm.

    Also declared: ComparatorChallenges/CoboundaryExpanders.lean:56 (same declaration text).

    def norm (X : Complex) (s i : ℕ) (f : X.Cochain i) : ℝ :=
    …

    Mentions: OAI.CoboundaryExpanders.Complex

11. def OAI.CoboundaryExpanders.Complex.coboundary line 60

    Source documentation

    Simplicial coboundary with coefficients in F₂.

    Also declared: ComparatorChallenges/CoboundaryExpanders.lean:60 (same declaration text).

    def coboundary (X : Complex) (i : ℕ) (f : X.Cochain i) : X.Cochain (i + 1) :=
    …

    Mentions: OAI.CoboundaryExpanders.Complex

12. def OAI.CoboundaryExpanders.Complex.coboundaries line 64

    Source documentation

    Actual coboundaries; in degree zero use constants, as in the manuscript.

    Also declared: ComparatorChallenges/CoboundaryExpanders.lean:64 (same declaration text).

    def coboundaries (X : Complex) : (i : ℕ) → Set (X.Cochain i)
      | 0 => {f | ∃ c : ZMod 2, f = fun _ => c}
      | i + 1 => Set.range (X.coboundary i)

    Mentions: OAI.CoboundaryExpanders.Complex

13. def OAI.CoboundaryExpanders.Complex.cocycles line 68
14. def OAI.CoboundaryExpanders.Complex.distance line 73

    Source documentation

    Distance in the source norm. On a nonempty subspace of this finite cochain space the infimum is a minimum; no closure or cocycle relaxation is used.

    Also declared: ComparatorChallenges/CoboundaryExpanders.lean:69 (same declaration text).

    def distance (X : Complex) (s i : ℕ) (f : X.Cochain i)
        (A : Set (X.Cochain i)) : ℝ :=
    …

    Mentions: OAI.CoboundaryExpanders.Complex

15. def OAI.CoboundaryExpanders.Complex.topDegree line 78

    Source documentation

    Number of top-dimensional faces incident to the given vertex.

    Also declared: ComparatorChallenges/CoboundaryExpanders.lean:74 (same declaration text).

    def topDegree (X : Complex) (s : ℕ) (v : Fin X.vertexCount) : ℕ :=
    …

    Mentions: OAI.CoboundaryExpanders.Complex

16. def OAI.CoboundaryExpanders.MainStatement line 86

    Source documentation

    The complete main assertion thm:main. Both constants are chosen outside all three quantifiers m, i, and f. Vertex growth is convergence to infinity, not mere existence of one arbitrarily large complex.

    Also declared: ComparatorChallenges/CoboundaryExpanders.lean:80 (same declaration text).

    def MainStatement : Prop :=
    …

17. theorem OAI.CoboundaryExpanders.Complex.mem_facesOf line 118
18. theorem OAI.CoboundaryExpanders.Complex.face_card line 122
19. theorem OAI.CoboundaryExpanders.Complex.face_mem line 125
20. theorem OAI.CoboundaryExpanders.Complex.weight_nonneg line 128
21. theorem OAI.CoboundaryExpanders.Complex.weight_pos line 132
22. theorem OAI.CoboundaryExpanders.Complex.norm_zero line 141
23. theorem OAI.CoboundaryExpanders.Complex.norm_nonneg line 144
24. theorem OAI.CoboundaryExpanders.Complex.norm_eq_zero_iff line 152
25. theorem OAI.CoboundaryExpanders.Complex.coboundary_zero line 171
26. theorem OAI.CoboundaryExpanders.Complex.coboundary_add line 175
27. theorem OAI.CoboundaryExpanders.Complex.coboundary_smul line 183
28. def OAI.CoboundaryExpanders.Complex.coboundaryLinear line 191
29. theorem OAI.CoboundaryExpanders.Complex.zero_mem_coboundaries line 196
30. theorem OAI.CoboundaryExpanders.Complex.coboundaries_nonempty line 202
31. theorem OAI.CoboundaryExpanders.Complex.distance_attained line 205
32. theorem OAI.CoboundaryExpanders.Complex.distance_nonneg line 213
33. theorem OAI.CoboundaryExpanders.Complex.distance_le_norm line 220
34. theorem OAI.CoboundaryExpanders.Complex.distance_eq_zero_iff line 227
35. theorem OAI.CoboundaryExpanders.Complex.cocycle_mem_coboundaries_of_expansion line 240
36. theorem OAI.CoboundaryExpanders.Complex.card_between_faces line 253
37. theorem OAI.CoboundaryExpanders.Complex.coboundary_coboundary line 277
38. theorem OAI.CoboundaryExpanders.Complex.sum_face_eq line 305
39. def OAI.CoboundaryExpanders.Complex.cofaceCount line 310
40. theorem OAI.CoboundaryExpanders.Complex.cofaceCount_eq_sum line 313
41. theorem OAI.CoboundaryExpanders.Complex.sum_cofaceCount line 318
42. theorem OAI.CoboundaryExpanders.Complex.sum_cofaceCount_real line 347
43. theorem OAI.CoboundaryExpanders.Complex.facesOf_nonempty_of_pure line 352
44. theorem OAI.CoboundaryExpanders.Complex.weight_eq_cofaceCount line 361
45. theorem OAI.CoboundaryExpanders.Complex.weight_averaging line 365
46. theorem OAI.CoboundaryExpanders.Complex.cofaceCount_self line 397
47. theorem OAI.CoboundaryExpanders.Complex.weight_top line 411
48. def OAI.CoboundaryExpanders.Complex.skeletonScale line 415
49. theorem OAI.CoboundaryExpanders.Complex.skeletonScale_pos line 418
50. theorem OAI.CoboundaryExpanders.Complex.skeletonScale_mul_topweight line 425
51. theorem OAI.CoboundaryExpanders.Complex.skeleton_topweight_comparison line 436
52. theorem OAI.CoboundaryExpanders.Complex.skeleton_weight_comparison line 450
53. theorem OAI.CoboundaryExpanders.Complex.norm_le_of_weight_le line 495
54. theorem OAI.CoboundaryExpanders.Complex.distance_le_of_weight_le line 505
55. theorem OAI.CoboundaryExpanders.Complex.skeleton_norm_comparison line 513
56. theorem OAI.CoboundaryExpanders.Complex.skeleton_distance_comparison line 529
57. theorem OAI.CoboundaryExpanders.Complex.skeleton_expansion_on_common_cochains line 547
58. def OAI.CoboundaryExpanders.Complex.skeleton line 576
59. theorem OAI.CoboundaryExpanders.Complex.mem_skeleton_faces line 586
60. theorem OAI.CoboundaryExpanders.Complex.skeleton_facesOf line 590
61. theorem OAI.CoboundaryExpanders.Complex.skeleton_pure line 598
62. theorem OAI.CoboundaryExpanders.Complex.skeleton_connected line 613
63. def OAI.CoboundaryExpanders.Complex.skeletonFaceEquiv line 622
64. theorem OAI.CoboundaryExpanders.Complex.skeletonFaceEquiv_val line 626
65. theorem OAI.CoboundaryExpanders.Complex.skeletonFaceEquiv_symm_val line 629
66. def OAI.CoboundaryExpanders.Complex.skeletonCochainEquiv line 632
67. theorem OAI.CoboundaryExpanders.Complex.skeletonCochainEquiv_apply line 636
68. theorem OAI.CoboundaryExpanders.Complex.skeleton_weight line 640
69. theorem OAI.CoboundaryExpanders.Complex.skeleton_norm line 645
70. theorem OAI.CoboundaryExpanders.Complex.skeleton_coboundary line 653
71. theorem OAI.CoboundaryExpanders.Complex.skeleton_distance_image line 665
72. theorem OAI.CoboundaryExpanders.Complex.skeleton_coboundaries line 679
73. theorem OAI.CoboundaryExpanders.Complex.skeleton_expansion line 699
74. def OAI.CoboundaryExpanders.Complex.vertexFaceEquiv line 714
75. theorem OAI.CoboundaryExpanders.Complex.vertexFaceEquiv_val line 724
76. theorem OAI.CoboundaryExpanders.Complex.card_facesOf_zero line 727
77. theorem OAI.CoboundaryExpanders.Complex.coboundary_zero_degree line 731
78. theorem OAI.CoboundaryExpanders.Complex.coboundary_const line 737
79. theorem OAI.CoboundaryExpanders.Complex.coboundaries_subset_cocycles line 745
80. theorem OAI.CoboundaryExpanders.Complex.cocycles_zero_eq_coboundaries_of_connected line 755