def HallTheorem.BipartiteExpander {L : Type u_1} {R : Type u_2} [DecidableEq R] [Fintype L] (neighbors : L → Finset R) (α β : ℝ) : Prop

theorem HallTheorem.hall_marriage_theorem {L : Type u_1} {R : Type u_2} [Finite L] [DecidableEq R] (neighbors : L → Finset R) : (∀ (S : Finset L), S.card ≤ (S.biUnion neighbors).card) ↔ ∃ (f : L → R), Function.Injective f ∧ ∀ (x : L), f x ∈ neighbors x

theorem HallTheorem.bipartite_expander_matching {L : Type u_1} {R : Type u_2} [DecidableEq L] [DecidableEq R] [Fintype L] (neighbors : L → Finset R) (α β : ℝ) (hexp : BipartiteExpander neighbors α β) (hβ : 1 < β) (S : Finset L) (hS : ↑S.card ≤ α * ↑(Fintype.card L)) : ∃ (f : ↥S → R), Function.Injective f ∧ ∀ (x : ↥S), f x ∈ neighbors ↑x

structure HallTheorem.MultibutterflyNetwork (N numLayers : ℕ) : Type

• α : ℝ
• β : ℝ
• hβ : 1 < self.β
• upNeighbors : Fin numLayers → Fin N → Finset (Fin N)
• downNeighbors : Fin numLayers → Fin N → Finset (Fin N)
• upIsExpander (i : Fin numLayers) : BipartiteExpander (self.upNeighbors i) self.α self.β
• downIsExpander (i : Fin numLayers) : BipartiteExpander (self.downNeighbors i) self.α self.β

structure HallTheorem.LayerAssignment (N : ℕ) (α : ℝ) : Type

• up : Finset (Fin N)
• down : Finset (Fin N)
• disjoint : Disjoint self.up self.down
• up_small : ↑self.up.card ≤ α * ↑N
• down_small : ↑self.down.card ≤ α * ↑N

def HallTheorem.RoutingAssignment (N numLayers : ℕ) (α : ℝ) : Type

theorem HallTheorem.multibutterfly_can_route {N numLayers : ℕ} (net : MultibutterflyNetwork N numLayers) (assignments : RoutingAssignment N numLayers net.α) (i : Fin numLayers) : (∃ (fUp : ↥(assignments i).up → Fin N), Function.Injective fUp ∧ ∀ (x : ↥(assignments i).up), fUp x ∈ net.upNeighbors i ↑x) ∧ ∃ (fDown : ↥(assignments i).down → Fin N), Function.Injective fDown ∧ ∀ (x : ↥(assignments i).down), fDown x ∈ net.downNeighbors i ↑x

def HallTheorem.uniqueNeighbors {L : Type u_1} {R : Type u_2} [DecidableEq L] [DecidableEq R] (neighbors : L → Finset R) (S : Finset L) : Finset R

theorem HallTheorem.unique_neighbors_lower_bound {L : Type u_1} {R : Type u_2} [DecidableEq R] (neighbors : L → Finset R) (d : ℕ) (β : ℝ) (S : Finset L) (hexp : β * ↑S.card ≤ ↑(S.biUnion neighbors).card) (A B : Finset R) (hAB_union : A ∪ B = S.biUnion neighbors) (hAB_disj : Disjoint A B) (hedge : ↑A.card + 2 * ↑B.card ≤ ↑d * ↑S.card) : (2 * β - ↑d) * ↑S.card ≤ ↑A.card

def SimpleGraph.rightDegreeInS {L : Type u_1} {R : Type u_2} (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) (r : R) : ℕ

def SimpleGraph.uniqueNeighbors {L : Type u_1} {R : Type u_2} [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : Finset R

def SimpleGraph.multiNeighbors {L : Type u_1} {R : Type u_2} [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : Finset R

def SimpleGraph.IsBipartiteOn {L : Type u_1} {R : Type u_2} (G : SimpleGraph (L ⊕ R)) : Prop

theorem SimpleGraph.bipartiteNeighborFinset_eq_filter_pos {L : Type u_1} {R : Type u_2} [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : G.bipartiteNeighborFinset S = {r : R | 0 < G.rightDegreeInS S r}

theorem SimpleGraph.bipartiteNeighborFinset_eq_unique_union_multi {L : Type u_1} {R : Type u_2} [Fintype R] [DecidableEq R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : G.bipartiteNeighborFinset S = G.uniqueNeighbors S ∪ G.multiNeighbors S

theorem SimpleGraph.uniqueNeighbors_disjoint_multiNeighbors {L : Type u_1} {R : Type u_2} [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : Disjoint (G.uniqueNeighbors S) (G.multiNeighbors S)

theorem SimpleGraph.card_filter_adj_right_eq_of_regular_bipartite {L : Type u_1} {R : Type u_2} [Fintype L] [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] {d : ℕ} (hbip : G.IsBipartiteOn) (hreg : G.IsRegularOfDegree d) (l : L) : {r : R | G.Adj (Sum.inl l) (Sum.inr r)}.card = d

theorem SimpleGraph.sum_leftRightDegree_eq_d_mul_card {L : Type u_1} {R : Type u_2} [Fintype L] [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] {d : ℕ} (hbip : G.IsBipartiteOn) (hreg : G.IsRegularOfDegree d) (S : Finset L) : ∑ l ∈ S, {r : R | G.Adj (Sum.inl l) (Sum.inr r)}.card = d * S.card

theorem SimpleGraph.double_count_edges {L : Type u_1} {R : Type u_2} [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : ∑ l ∈ S, {r : R | G.Adj (Sum.inl l) (Sum.inr r)}.card = ∑ r : R, G.rightDegreeInS S r

theorem SimpleGraph.sum_rightDegreeInS_ge {L : Type u_1} {R : Type u_2} [Fintype R] [DecidableEq R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : ∑ r : R, G.rightDegreeInS S r ≥ (G.uniqueNeighbors S).card + 2 * (G.multiNeighbors S).card

theorem SimpleGraph.unique_neighbors_lower_bound {L : Type u_1} {R : Type u_2} [Fintype L] [Fintype R] [DecidableEq R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] {d : ℕ} {α β : ℝ} (hbip : G.IsBipartiteOn) (hreg : G.IsRegularOfDegree d) (hexp : G.IsBipartiteExpander α β) (S : Finset L) (hS : ↑S.card ≤ α * ↑(Fintype.card L)) : ↑(G.uniqueNeighbors S).card ≥ (2 * β - ↑d) * ↑S.card