structure Matchings.BipartiteGraph (n : ℕ) : Type

• Adj : Fin n → Fin n → Prop
• decAdj : DecidablePred fun (p : Fin n × Fin n) => self.Adj p.1 p.2

@[implicit_reducible]

instance Matchings.BipartiteGraph.instDecidableAdj {n : ℕ} (G : BipartiteGraph n) (u v : Fin n) : Decidable (G.Adj u v)

def Matchings.BipartiteGraph.leftNeighbors {n : ℕ} (G : BipartiteGraph n) (u : Fin n) : Finset (Fin n)

def Matchings.BipartiteGraph.rightNeighbors {n : ℕ} (G : BipartiteGraph n) (v : Fin n) : Finset (Fin n)

def Matchings.BipartiteGraph.denseLeft {n : ℕ} (G : BipartiteGraph n) : Prop

def Matchings.BipartiteGraph.denseRight {n : ℕ} (G : BipartiteGraph n) : Prop

structure Matchings.PartialMatching {n : ℕ} (G : BipartiteGraph n) : Type

• edges : Finset (Fin n × Fin n)
• edge_adj (p : Fin n × Fin n) : p ∈ self.edges → G.Adj p.1 p.2
• left_inj ⦃p q : Fin n × Fin n⦄ : p ∈ self.edges → q ∈ self.edges → p.1 = q.1 → p = q
• right_inj ⦃p q : Fin n × Fin n⦄ : p ∈ self.edges → q ∈ self.edges → p.2 = q.2 → p = q

def Matchings.PartialMatching.matchedLeft {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Finset (Fin n)

def Matchings.PartialMatching.matchedRight {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Finset (Fin n)

def Matchings.PartialMatching.unmatchedLeft {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Finset (Fin n)

def Matchings.PartialMatching.unmatchedRight {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Finset (Fin n)

theorem Matchings.PartialMatching.fst_injOn_edges {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Set.InjOn Prod.fst ↑M.edges

theorem Matchings.PartialMatching.matchedLeft_card {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : M.matchedLeft.card = M.edges.card

def Matchings.HasAugPath1 {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Prop

def Matchings.HasAugPath3 {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Prop

def Matchings.HasAugPathLE3 {n : ℕ} {G : BipartiteGraph n} (M : PartialMatching G) : Prop

theorem Matchings.augmenting_path_of_min_degree {n : ℕ} {G : BipartiteGraph n} {M : PartialMatching G} (hLeft : G.denseLeft) (hRight : G.denseRight) (hu : M.unmatchedLeft.Nonempty) (hv : M.unmatchedRight.Nonempty) : HasAugPathLE3 M

theorem Matchings.geom_contraction_bound (r : ℝ) (hr_pos : 0 < r) (S : ℕ → ℕ) (hcontract : ∀ (i : ℕ), ↑(S (i + 1)) ≤ r * ↑(S i)) (k : ℕ) : ↑(S k) ≤ r ^ k * ↑(S 0)

theorem Matchings.pow_mul_lt_one_of_log_bound (N : ℕ) (hN : 0 < N) (r : ℝ) (hr_pos : 0 < r) (hr_lt : r < 1) (k : ℕ) (hk : ↑k > Real.log ↑N / Real.log (1 / r)) : r ^ k * ↑N < 1

theorem Matchings.matching_terminates_log_steps (N d : ℕ) (β : ℝ) (hd_pos : 0 < d) (hβ_bound : β > ↑d / 2) (hβ_lt_d : β < ↑d) (S : ℕ → ℕ) (hS0 : S 0 ≤ N) (hcontract : ∀ (i : ℕ), ↑(S (i + 1)) ≤ 2 * (1 - β / ↑d) * ↑(S i)) : ∃ k ≤ ⌈Real.log ↑N / Real.log (1 / (2 * (1 - β / ↑d)))⌉₊ + 1, S k = 0

structure Matchings.SizedMatching {n : ℕ} (G : BipartiteGraph n) (k : ℕ) : Type

• edges : Finset (Fin n × Fin n)
• edge_adj (p : Fin n × Fin n) : p ∈ self.edges → G.Adj p.1 p.2
• left_inj ⦃p q : Fin n × Fin n⦄ : p ∈ self.edges → q ∈ self.edges → p.1 = q.1 → p = q
• right_inj ⦃p q : Fin n × Fin n⦄ : p ∈ self.edges → q ∈ self.edges → p.2 = q.2 → p = q
• card_eq : self.edges.card = k

@[implicit_reducible]

instance Matchings.sizedMatchingDecEq {n : ℕ} {G : BipartiteGraph n} {k : ℕ} : DecidableEq (SizedMatching G k)

@[implicit_reducible]

noncomputable instance Matchings.sizedMatchingFintype {n : ℕ} {G : BipartiteGraph n} {k : ℕ} : Fintype (SizedMatching G k)

def Matchings.ChainVertex {n : ℕ} (G : BipartiteGraph n) : Type

@[implicit_reducible]

noncomputable instance Matchings.chainVertexFintype {n : ℕ} {G : BipartiteGraph n} : Fintype (ChainVertex G)

@[implicit_reducible]

instance Matchings.chainVertexDecEq {n : ℕ} {G : BipartiteGraph n} : DecidableEq (ChainVertex G)

@[reducible, inline]

abbrev Matchings.PerfMatching {n : ℕ} (G : BipartiteGraph n) : Type

structure Matchings.Transition {n : ℕ} (G : BipartiteGraph n) : Type

• source : ChainVertex G
• target : ChainVertex G

def Matchings.chainIsAdj {n : ℕ} {G : BipartiteGraph n} (v w : ChainVertex G) : Prop

def Matchings.matchingSymDiff {n : ℕ} {G : BipartiteGraph n} (s t : PerfMatching G) : Finset (Fin n × Fin n)

def Matchings.chainVertexEdges {n : ℕ} {G : BipartiteGraph n} : ChainVertex G → Finset (Fin n × Fin n)

theorem Matchings.encoding_source_recovery {α : Type u_1} [DecidableEq α] {s₁ s₂ P R : Finset α} (hP₁ : Disjoint P s₁) (hP₂ : Disjoint P s₂) (hR₁ : R ⊆ s₁) (hR₂ : R ⊆ s₂) (heq : s₁ \ R ∪ P = s₂ \ R ∪ P) : s₁ = s₂

theorem Matchings.symDiff_determines_target {n : ℕ} {G : BipartiteGraph n} {s t₁ t₂ : PerfMatching G} (hD : matchingSymDiff s t₁ = matchingSymDiff s t₂) : t₁ = t₂

structure Matchings.TypeBPathData {n : ℕ} {G : BipartiteGraph n} (T : Transition G) (s t : PerfMatching G) : Type

• removed : Finset (Fin n × Fin n)
• added : Finset (Fin n × Fin n)
• removed_sub : self.removed ⊆ s.edges
• added_disj : Disjoint self.added s.edges
• removed_sub_symDiff : self.removed ⊆ s.edges \ t.edges
• added_sub_symDiff : self.added ⊆ t.edges \ s.edges
• encodingVertex : ChainVertex G
• encoding_edges_eq : chainVertexEdges self.encodingVertex = s.edges \ self.removed ∪ self.added
• canonRemoved : Finset (Fin n × Fin n)
• removed_eq_canon : self.removed = self.canonRemoved
• canonAdded : Finset (Fin n × Fin n)
• added_eq_canon : self.added = self.canonAdded
• canon_removed_spec : self.canonRemoved = chainVertexEdges T.source \ chainVertexEdges self.encodingVertex
• canon_added_spec : self.canonAdded = chainVertexEdges self.encodingVertex \ chainVertexEdges T.source
• canonSymDiff : Finset (Fin n × Fin n)
• symDiff_eq_canon : matchingSymDiff s t = self.canonSymDiff
• canon_symDiff_spec : self.canonSymDiff = s.edges \ chainVertexEdges self.encodingVertex ∪ chainVertexEdges self.encodingVertex \ s.edges

def Matchings.transitionEncoding {n : ℕ} {G : BipartiteGraph n} {T : Transition G} {s t : PerfMatching G} (data : TypeBPathData T s t) : ChainVertex G

def Matchings.typeBUsesTransition {n : ℕ} {G : BipartiteGraph n} (T : Transition G) (s t : PerfMatching G) : Prop

theorem Matchings.encoding_determines_source_from_structure {n : ℕ} {G : BipartiteGraph n} {T : Transition G} {s₁ t₁ s₂ t₂ : PerfMatching G} (d₁ : TypeBPathData T s₁ t₁) (d₂ : TypeBPathData T s₂ t₂) (heq : d₁.encodingVertex = d₂.encodingVertex) : s₁ = s₂

theorem Matchings.encoding_determines_symDiff_from_structure {n : ℕ} {G : BipartiteGraph n} {T : Transition G} {s₁ t₁ s₂ t₂ : PerfMatching G} (d₁ : TypeBPathData T s₁ t₁) (d₂ : TypeBPathData T s₂ t₂) (heq : d₁.encodingVertex = d₂.encodingVertex) : matchingSymDiff s₁ t₁ = matchingSymDiff s₂ t₂

theorem Matchings.transition_bound {n : ℕ} {G : BipartiteGraph n} (T : Transition G) (hT : chainIsAdj T.source T.target) : {p : PerfMatching G × PerfMatching G | typeBUsesTransition T p.1 p.2}.card ≤ Fintype.card (ChainVertex G)

noncomputable def Matchings.partner {n : ℕ} {G : BipartiteGraph n} (augment : SizedMatching G (n - 1) → PerfMatching G) (v : ChainVertex G) : PerfMatching G

noncomputable def Matchings.partnerPreimage {n : ℕ} {G : BipartiteGraph n} (augment : SizedMatching G (n - 1) → PerfMatching G) (s : PerfMatching G) : Finset (ChainVertex G)

inductive Matchings.PartnerWitness (n : ℕ) : Type

• self {n : ℕ} : PartnerWitness n
• reduced {n : ℕ} : Fin n → PartnerWitness n
• reducedRotated {n : ℕ} : Fin n → Fin n → PartnerWitness n

def Matchings.partnerWitnessEquiv (n : ℕ) : PartnerWitness n ≃ Unit ⊕ Fin n ⊕ Fin n × Fin n

@[implicit_reducible]

instance Matchings.partnerWitnessFintype {n : ℕ} : Fintype (PartnerWitness n)

theorem Matchings.card_partnerWitness (n : ℕ) : Fintype.card (PartnerWitness n) = 1 + n + n * n

theorem Matchings.partnerWitness_card_le (n : ℕ) : Fintype.card (PartnerWitness n) ≤ (n + 1) ^ 2

theorem Matchings.partner_preimage_card_le_exact {n : ℕ} {G : BipartiteGraph n} (hn : 0 < n) (augment : SizedMatching G (n - 1) → PerfMatching G) (s : PerfMatching G) (h_edges_diff : ∀ (m : SizedMatching G (n - 1)), augment m = s → (m.edges \ s.edges).card ≤ 1) : (partnerPreimage augment s).card ≤ 1 + n + n * n

theorem Matchings.partner_preimage_card_le {n : ℕ} {G : BipartiteGraph n} (hn : 0 < n) (augment : SizedMatching G (n - 1) → PerfMatching G) (s : PerfMatching G) (h_edges_diff : ∀ (m : SizedMatching G (n - 1)), augment m = s → (m.edges \ s.edges).card ≤ 1) : (partnerPreimage augment s).card ≤ (n + 1) ^ 2

def Matchings.HasConductanceLB {V : Type u_1} [Fintype V] [DecidableEq V] (cutEdges vol : Finset V → ℝ) (c : ℝ) : Prop

def Matchings.HasConductanceUB {V : Type u_1} [Fintype V] [DecidableEq V] (cutEdges vol : Finset V → ℝ) (c : ℝ) : Prop

theorem Matchings.canonical_paths_cut_bound (cutEdges_S vol_S S_card b d_max : ℝ) (hb_pos : 0 < b) (hd_pos : 0 < d_max) (hvol_pos : 0 < vol_S) (hcut : cutEdges_S ≥ S_card / (2 * b)) (hvol : vol_S ≤ S_card * d_max) : cutEdges_S / vol_S ≥ 1 / (2 * b * d_max)

noncomputable def Matchings.chainDegree {n : ℕ} {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (v : ChainVertex G) : ℕ

noncomputable def Matchings.chainVol {n : ℕ} {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (S : Finset (ChainVertex G)) : ℝ

noncomputable def Matchings.chainCutEdges {n : ℕ} {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (S : Finset (ChainVertex G)) : ℝ

theorem Matchings.matching_chain_conductance_bound {n : ℕ} (hn : 0 < n) {G : BipartiteGraph n} (cutEdges vol : Finset (ChainVertex G) → ℝ) (hvol_pos : ∀ (S : Finset (ChainVertex G)), S.Nonempty → 0 < vol S) (hmax_degree : ∀ (S : Finset (ChainVertex G)), vol S ≤ ↑S.card * ↑n ^ 2) (hcongestion : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → cutEdges S ≥ ↑S.card / (2 * (↑n + 1) ^ 4)) : HasConductanceLB cutEdges vol (1 / (2 * (↑n + 1) ^ 4 * ↑n ^ 2))

theorem Matchings.matching_chain_conductance_concrete {n : ℕ} (hn : 0 < n) {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (hmin_deg : ∀ (v : ChainVertex G), 0 < (neighbors v).card) (hmax_deg : ∀ (v : ChainVertex G), (neighbors v).card ≤ n ^ 2) (hcongestion : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → chainCutEdges neighbors S ≥ ↑S.card / (2 * (↑n + 1) ^ 4)) : HasConductanceLB (chainCutEdges neighbors) (chainVol neighbors) (1 / (2 * (↑n + 1) ^ 4 * ↑n ^ 2))

theorem Matchings.matching_chain_conductance_theta {n : ℕ} (hn : 0 < n) {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (hmin_deg : ∀ (v : ChainVertex G), 0 < (neighbors v).card) (hmax_deg : ∀ (v : ChainVertex G), (neighbors v).card ≤ n ^ 2) (hcongestion : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → chainCutEdges neighbors S ≥ ↑S.card / (2 * (↑n + 1) ^ 4)) : HasConductanceLB (chainCutEdges neighbors) (chainVol neighbors) (1 / (2 * (↑n + 1) ^ 6))

theorem Matchings.matching_chain_conductance_upper_bound {n : ℕ} (hn : 0 < n) {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (hmin_deg : ∀ (v : ChainVertex G), 0 < (neighbors v).card) (hmax_deg : ∀ (v : ChainVertex G), (neighbors v).card ≤ n ^ 2) : HasConductanceUB (chainCutEdges neighbors) (chainVol neighbors) (2 * (1 / ↑n ^ 6))

theorem Matchings.chain_congestion_bound {n : ℕ} (_hn : 0 < n) {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (_hmin_deg : ∀ (v : ChainVertex G), 0 < (neighbors v).card) (_hmax_deg : ∀ (v : ChainVertex G), (neighbors v).card ≤ n ^ 2) (hpaths : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → ↑S.card * ↑(Finset.univ \ S).card ≤ chainCutEdges neighbors S * (↑n + 1) ^ 4) (S : Finset (ChainVertex G)) : S.Nonempty → S ≠ Finset.univ → chainCutEdges neighbors S ≥ ↑S.card / (2 * (↑n + 1) ^ 4)

theorem Matchings.chain_canonical_paths_crossing {n : ℕ} (hn : 0 < n) {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (hmin_deg : ∀ (v : ChainVertex G), 0 < (neighbors v).card) (hmax_deg : ∀ (v : ChainVertex G), (neighbors v).card ≤ n ^ 2) (path_assign : Finset (ChainVertex G) → ChainVertex G → ChainVertex G → ChainVertex G × ChainVertex G) (hassign_valid : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → ∀ s ∈ S, ∀ t ∈ Finset.univ \ S, (path_assign S s t).1 ∈ S ∧ (path_assign S s t).2 ∈ {x ∈ neighbors (path_assign S s t).1 | x ∉ S}) (hassign_bound : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → ∀ v ∈ S, ∀ w ∈ {x ∈ neighbors v | x ∉ S}, {p ∈ S ×ˢ (Finset.univ \ S) | path_assign S p.1 p.2 = (v, w)}.card ≤ (n + 1) ^ 4) (S : Finset (ChainVertex G)) : S.Nonempty → S ≠ Finset.univ → ↑S.card * ↑(Finset.univ \ S).card ≤ chainCutEdges neighbors S * (↑n + 1) ^ 4

theorem Matchings.matching_chain_conductance_theta_full {n : ℕ} (hn : 0 < n) {G : BipartiteGraph n} (neighbors : ChainVertex G → Finset (ChainVertex G)) (hmin_deg : ∀ (v : ChainVertex G), 0 < (neighbors v).card) (hmax_deg : ∀ (v : ChainVertex G), (neighbors v).card ≤ n ^ 2) (path_assign : Finset (ChainVertex G) → ChainVertex G → ChainVertex G → ChainVertex G × ChainVertex G) (hassign_valid : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → ∀ s ∈ S, ∀ t ∈ Finset.univ \ S, (path_assign S s t).1 ∈ S ∧ (path_assign S s t).2 ∈ {x ∈ neighbors (path_assign S s t).1 | x ∉ S}) (hassign_bound : ∀ (S : Finset (ChainVertex G)), S.Nonempty → S ≠ Finset.univ → ∀ v ∈ S, ∀ w ∈ {x ∈ neighbors v | x ∉ S}, {p ∈ S ×ˢ (Finset.univ \ S) | path_assign S p.1 p.2 = (v, w)}.card ≤ (n + 1) ^ 4) : HasConductanceLB (chainCutEdges neighbors) (chainVol neighbors) (1 / (2 * (↑n + 1) ^ 6)) ∧ HasConductanceUB (chainCutEdges neighbors) (chainVol neighbors) (2 * (1 / ↑n ^ 6))

def Matchings.permanent {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ℝ