Fractional rounding with bounded incidence discrepancy

noncomputable def Nibble.BeckFiala.floating {V : Type u_1} (H : Finset (Finset V)) (y : Finset V → ℝ) : Finset (Finset V)

The floating edges of a fractional selection: those whose value is neither 0 nor 1.

Equations

• Nibble.BeckFiala.floating H y = {t ∈ H | y t ≠ 0 ∧ y t ≠ 1}

theorem Nibble.BeckFiala.floating_subset {V : Type u_1} (H : Finset (Finset V)) (y : Finset V → ℝ) : floating H y ⊆ H

theorem Nibble.BeckFiala.notMem_floating_iff {V : Type u_1} {H : Finset (Finset V)} {y : Finset V → ℝ} {t : Finset V} (ht : t ∈ H) : t ∉ floating H y ↔ y t = 0 ∨ y t = 1

noncomputable def Nibble.BeckFiala.active {V : Type u_1} [DecidableEq V] (F : Finset (Finset V)) (k : ℕ) : Finset V

The active vertices of a floating set: those meeting more than k floating edges.

Equations

• Nibble.BeckFiala.active F k = {x ∈ F.biUnion id | k < {t ∈ F | x ∈ t}.card}

theorem Nibble.BeckFiala.mem_active_iff {V : Type u_1} [DecidableEq V] {F : Finset (Finset V)} {k : ℕ} {x : V} : x ∈ active F k ↔ k < {t ∈ F | x ∈ t}.card

theorem Nibble.BeckFiala.card_active_lt {V : Type u_1} [DecidableEq V] {F : Finset (Finset V)} {k : ℕ} (hk : ∀ t ∈ F, t.card ≤ k) (hF : F.Nonempty) : (active F k).card < F.card

Few active vertices. If every edge of the floating family meets at most k vertices and the family is nonempty, then there are strictly fewer active vertices than floating edges.

theorem Nibble.BeckFiala.exists_kernel_vector {V : Type u_1} [DecidableEq V] {F : Finset (Finset V)} {k : ℕ} (hk : ∀ t ∈ F, t.card ≤ k) (hF : F.Nonempty) : ∃ (U : Finset V → ℝ), (∀ t ∉ F, U t = 0) ∧ (∃ t ∈ F, U t ≠ 0) ∧ ∀ x ∈ active F k, ∑ t ∈ F with x ∈ t, U t = 0

Existence of a nonzero vector annihilated by all active constraints.

theorem Nibble.BeckFiala.exists_step {V : Type u_1} [DecidableEq V] (k : ℕ) (H : Finset (Finset V)) (hk : ∀ t ∈ H, t.card ≤ k) (y : Finset V → ℝ) (hy0 : ∀ t ∈ H, 0 ≤ y t) (hy1 : ∀ t ∈ H, y t ≤ 1) (hF : (floating H y).Nonempty) : ∃ (y' : Finset V → ℝ), (∀ t ∈ H, 0 ≤ y' t) ∧ (∀ t ∈ H, y' t ≤ 1) ∧ (∀ t ∉ floating H y, y' t = y t) ∧ (floating H y').card < (floating H y).card ∧ ∀ (x : V), k < {t ∈ floating H y | x ∈ t}.card → ∑ t ∈ H with x ∈ t, y' t = ∑ t ∈ H with x ∈ t, y t

One rounding step. Given a fractional selection with a nonempty floating set, there is another one with strictly fewer floating edges, which agrees with the old one off the floating set and has exactly the same degree at every active vertex.

theorem Nibble.BeckFiala.exists_rounding {V : Type u_1} [DecidableEq V] (k : ℕ) (H : Finset (Finset V)) (hk : ∀ t ∈ H, t.card ≤ k) (y : Finset V → ℝ) (hy0 : ∀ t ∈ H, 0 ≤ y t) (hy1 : ∀ t ∈ H, y t ≤ 1) : ∃ S ⊆ H, (∀ t ∈ H, y t = 1 → t ∈ S) ∧ (∀ t ∈ H, y t = 0 → t ∉ S) ∧ ∀ (x : V), |↑{t ∈ S | x ∈ t}.card - ∑ t ∈ H with x ∈ t, y t| ≤ ↑k

Beck–Fiala rounding. If every edge of H has at most k vertices, every fractional selection y : H → [0,1] can be rounded to a subfamily S ⊆ H (keeping the edges of value 1 and discarding those of value 0) whose degree at every vertex differs from the fractional degree by at most k.

Simultaneous fractional rounding of degrees and codegrees

def Nibble.BeckFiala.pairClosure {V : Type u_1} (T : Finset V) : Finset (Finset V)

The subsets of T of size at most 2.

Equations

• Nibble.BeckFiala.pairClosure T = {s ∈ T.powerset | s.card ≤ 2}

theorem Nibble.BeckFiala.mem_pairClosure {V : Type u_1} {T s : Finset V} : s ∈ pairClosure T ↔ s ⊆ T ∧ s.card ≤ 2

theorem Nibble.BeckFiala.biUnion_pairClosure {V : Type u_1} [DecidableEq V] (T : Finset V) : (pairClosure T).biUnion id = T

T is recovered from pairClosure T as the union of its members.

theorem Nibble.BeckFiala.pairClosure_injective {V : Type u_1} : Function.Injective pairClosure

theorem Nibble.BeckFiala.singleton_mem_pairClosure {V : Type u_1} {T : Finset V} {v : V} : {v} ∈ pairClosure T ↔ v ∈ T

theorem Nibble.BeckFiala.pair_mem_pairClosure {V : Type u_1} [DecidableEq V] {T : Finset V} {x z : V} : {x, z} ∈ pairClosure T ↔ x ∈ T ∧ z ∈ T

theorem Nibble.BeckFiala.card_pairClosure_le {V : Type u_1} (T : Finset V) : (pairClosure T).card ≤ 1 + T.card * T.card

The auxiliary vertex set of an edge has at most 1 + |T|² elements.

theorem Nibble.BeckFiala.exists_rounding_pairs {V : Type u_1} [DecidableEq V] (r : ℕ) (H : Finset (Finset V)) (hunif : ∀ T ∈ H, T.card = r) (y : Finset V → ℝ) (hy0 : ∀ T ∈ H, 0 ≤ y T) (hy1 : ∀ T ∈ H, y T ≤ 1) : ∃ S ⊆ H, (∀ (v : V), |↑{T ∈ S | v ∈ T}.card - ∑ T ∈ H with v ∈ T, y T| ≤ 1 + ↑r * ↑r) ∧ ∀ (x z : V), |↑{T ∈ S | x ∈ T ∧ z ∈ T}.card - ∑ T ∈ H with x ∈ T ∧ z ∈ T, y T| ≤ 1 + ↑r * ↑r

Beck–Fiala rounding with codegree control. Every fractional selection y : H → [0,1] of an r-uniform hypergraph H can be rounded to a subhypergraph S ⊆ H whose degrees and codegrees differ from the fractional degrees and codegrees by at most 1 + r².

Weighted hypergraph incidences

The fractional-rounding proof in Paper III uses edge weights rather than the unweighted near-regular hypotheses of nearRegularNibbleTheorem. These definitions retain the exact finite-set model of the frozen proof. The rounding theorem itself is not asserted here.

def Hypergraph.weightedLoad {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (w : Finset V → ℝ) (v : V) : ℝ

Total edge weight incident with a vertex.

Equations

• Hypergraph.weightedLoad H w v = ∑ e ∈ H with v ∈ e, w e

def Hypergraph.weightedCodegree {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (w : Finset V → ℝ) (u v : V) : ℝ

Total edge weight incident with both vertices.

Equations

• Hypergraph.weightedCodegree H w u v = ∑ e ∈ H with u ∈ e ∧ v ∈ e, w e

theorem Hypergraph.sum_weightedLoad {V : Type u_1} [Fintype V] [DecidableEq V] (H : Finset (Finset V)) (w : Finset V → ℝ) {r : ℕ} (hr : IsUniform H r) : ∑ v : V, weightedLoad H w v = ↑r * ∑ e ∈ H, w e

Weighted handshake for an r-uniform finite hypergraph.

theorem Hypergraph.weightedSum_le_card {V : Type u_1} [Fintype V] [DecidableEq V] (H : Finset (Finset V)) (w : Finset V → ℝ) {r : ℕ} (hr : IsUniform H r) (hload : ∀ (v : V), weightedLoad H w v ≤ 1) : ↑r * ∑ e ∈ H, w e ≤ ↑(Fintype.card V)

A fractional matching on an r-uniform hypergraph has total weight at most |V|/r.

def Hypergraph.BoundedEdgeWeightedRounding : Prop

Exact bounded-edge weighted-rounding target from the Paper III freeze. This is a specification, not a proof or a public result.

Equations

• One or more equations did not get rendered due to their size.

Weighted fractional-to-integral nibble bridge

theorem Nibble.fracNibble_spread_weightedCodegree (r : ℕ) (hr : 2 ≤ r) (β : ℝ) (hβ : 0 < β) : ∃ (δ : ℝ), 0 < δ ∧ ∃ (γ : ℝ), 0 < γ ∧ ∃ (η : ℝ), 0 < η ∧ ∀ {W : Type} [inst : Fintype W] [inst_1 : DecidableEq W] (H : Finset (Finset W)) (w : Finset W → ℝ) (Exc : Finset W), Hypergraph.IsUniform H r → (∀ (T : Finset W), 0 ≤ w T) → (∀ T ∈ H, w T ≤ δ) → (∀ (v : W), ∑ T ∈ H with v ∈ T, w T ≤ 1) → (∀ v ∉ Exc, 1 - γ ≤ ∑ T ∈ H with v ∈ T, w T) → ↑Exc.card ≤ η * ↑(Fintype.card W) → (∀ (x z : W), x ≠ z → ∑ T ∈ H with x ∈ T ∧ z ∈ T, w T ≤ γ) → ∃ (M : Finset (Finset W)), Hypergraph.IsMatching H M ∧ (1 - β) * (↑(Fintype.card W) / ↑r) ≤ ↑M.card ∧ (1 - β) * ∑ T ∈ H, w T ≤ ↑M.card

The weighted nibble for spread, near-perfect fractional matchings. No regularity and no codegree hypothesis is placed on the hypergraph: all the hypotheses are on the fractional matching w.

theorem Nibble.weight_le_weightedCodegree {W : Type} [DecidableEq W] {r : ℕ} (hr : 2 ≤ r) {H : Finset (Finset W)} {w : Finset W → ℝ} {γ : ℝ} (hunif : Hypergraph.IsUniform H r) (hwnn : ∀ (T : Finset W), 0 ≤ w T) (hcod : ∀ (x z : W), x ≠ z → ∑ T ∈ H with x ∈ T ∧ z ∈ T, w T ≤ γ) {T : Finset W} (hT : T ∈ H) : w T ≤ γ

The spread hypothesis is redundant. Every edge contains a pair x ≠ z, so its weight is at most the weighted codegree of that pair.

theorem Nibble.fracNibble_weightedCodegree (r : ℕ) (hr : 2 ≤ r) (β : ℝ) (hβ : 0 < β) : ∃ (γ : ℝ), 0 < γ ∧ ∃ (η : ℝ), 0 < η ∧ ∀ {W : Type} [inst : Fintype W] [inst_1 : DecidableEq W] (H : Finset (Finset W)) (w : Finset W → ℝ) (Exc : Finset W), Hypergraph.IsUniform H r → (∀ (T : Finset W), 0 ≤ w T) → (∀ (v : W), ∑ T ∈ H with v ∈ T, w T ≤ 1) → (∀ v ∉ Exc, 1 - γ ≤ ∑ T ∈ H with v ∈ T, w T) → ↑Exc.card ≤ η * ↑(Fintype.card W) → (∀ (x z : W), x ≠ z → ∑ T ∈ H with x ∈ T ∧ z ∈ T, w T ≤ γ) → ∃ (M : Finset (Finset W)), Hypergraph.IsMatching H M ∧ (1 - β) * (↑(Fintype.card W) / ↑r) ≤ ↑M.card ∧ (1 - β) * ∑ T ∈ H, w T ≤ ↑M.card

The weighted nibble for near-perfect fractional matchings of small weighted codegree. The spread hypothesis of Nibble.fracNibble_spread_weightedCodegree is dropped: it follows from the weighted codegree bound. Still no hypothesis whatsoever on the degrees or codegrees of H.

theorem Nibble.fracNibble_spread_codegree (r : ℕ) (hr : 2 ≤ r) (β : ℝ) (hβ : 0 < β) (C : ℝ) (hC : 0 < C) : ∃ (δ : ℝ), 0 < δ ∧ ∃ (γ : ℝ), 0 < γ ∧ ∃ (η : ℝ), 0 < η ∧ ∀ {W : Type} [inst : Fintype W] [inst_1 : DecidableEq W] (H : Finset (Finset W)) (w : Finset W → ℝ) (Exc : Finset W), Hypergraph.IsUniform H r → (∀ (x z : W), x ≠ z → ↑(Hypergraph.codegree H x z) ≤ C) → (∀ (T : Finset W), 0 ≤ w T) → (∀ T ∈ H, w T ≤ δ) → (∀ (v : W), ∑ T ∈ H with v ∈ T, w T ≤ 1) → (∀ v ∉ Exc, 1 - γ ≤ ∑ T ∈ H with v ∈ T, w T) → ↑Exc.card ≤ η * ↑(Fintype.card W) → ∃ (M : Finset (Finset W)), Hypergraph.IsMatching H M ∧ (1 - β) * (↑(Fintype.card W) / ↑r) ≤ ↑M.card ∧ (1 - β) * ∑ T ∈ H, w T ≤ ↑M.card

The weighted nibble for spread fractional matchings on hypergraphs of bounded codegree. A fractional matching with all weights at most δ on a hypergraph of codegree at most C has weighted codegree at most C·δ, so Nibble.fracNibble_spread_weightedCodegree applies. This generalises Nibble.exists_matching_of_spread (the case C = 1) to an arbitrary codegree bound, and adds the weighted form (1-β)∑w ≤ |M| of the conclusion to the covering form (1-β)|W|/r ≤ |M|.

Three-uniform weighted rounding with total slack

def Nibble.Slack.wLoad {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (v : X) : ℝ

The w-load of a vertex: the total weight of the edges through it.

Equations

• Nibble.Slack.wLoad K w v = ∑ T ∈ K with v ∈ T, w T

@[reducible, inline]

abbrev Nibble.Slack.Pad (X : Type) (m : ℕ) : Type

The padded vertex type: the real vertices together with 2m dummies, m on each side.

Equations

• Nibble.Slack.Pad X m = (X ⊕ Fin m × Bool)

def Nibble.Slack.mixTriple {X : Type} [DecidableEq X] (m : ℕ) (v : X) (i j : Fin m) : Finset (Pad X m)

The added triple joining the real vertex v to the left dummy i and the right dummy j.

Equations

• Nibble.Slack.mixTriple m v i j = {Sum.inl v, Sum.inr (i, false), Sum.inr (j, true)}

def Nibble.Slack.padFam {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) : Finset (Finset (Pad X m))

The padded hypergraph: the image of K together with all the mixed triples.

Equations

• Nibble.Slack.padFam K m = Finset.image (Finset.image Sum.inl) K ∪ Finset.image (fun (t : X × Fin m × Fin m) => Nibble.Slack.mixTriple m t.1 t.2.1 t.2.2) Finset.univ

noncomputable def Nibble.Slack.padWt {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) : Finset (Pad X m) → ℝ

The padded weighting.

Equations

• Nibble.Slack.padWt K w m U = if U.toRight = ∅ then w U.toLeft else (∑ v ∈ U.toLeft, (1 - Nibble.Slack.wLoad K w v)) / ↑m ^ 2

@[simp]

theorem Nibble.Slack.toLeft_image_inl {X : Type} [DecidableEq X] (m : ℕ) (T : Finset X) : (Finset.image Sum.inl T).toLeft = T

@[simp]

theorem Nibble.Slack.toRight_image_inl {X : Type} [DecidableEq X] (m : ℕ) (T : Finset X) : (Finset.image Sum.inl T).toRight = ∅

@[simp]

theorem Nibble.Slack.mixTriple_toLeft {X : Type} [DecidableEq X] (m : ℕ) (v : X) (i j : Fin m) : (mixTriple m v i j).toLeft = {v}

@[simp]

theorem Nibble.Slack.mixTriple_toRight {X : Type} [DecidableEq X] (m : ℕ) (v : X) (i j : Fin m) : (mixTriple m v i j).toRight = {(i, false), (j, true)}

theorem Nibble.Slack.mixTriple_card {X : Type} [DecidableEq X] (m : ℕ) (v : X) (i j : Fin m) : (mixTriple m v i j).card = 3

theorem Nibble.Slack.mem_mixTriple_inl {X : Type} [DecidableEq X] (m : ℕ) (v u : X) (i j : Fin m) : Sum.inl u ∈ mixTriple m v i j ↔ u = v

theorem Nibble.Slack.mem_mixTriple_inr {X : Type} [DecidableEq X] (m : ℕ) (v : X) (i j : Fin m) (d : Fin m × Bool) : Sum.inr d ∈ mixTriple m v i j ↔ d = (i, false) ∨ d = (j, true)

theorem Nibble.Slack.mixTriple_inj {X : Type} [DecidableEq X] (m : ℕ) {v v' : X} {i i' j j' : Fin m} (h : mixTriple m v i j = mixTriple m v' i' j') : v = v' ∧ i = i' ∧ j = j'

theorem Nibble.Slack.padWt_image_inl {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (T : Finset X) : padWt K w m (Finset.image Sum.inl T) = w T

theorem Nibble.Slack.padWt_mixTriple {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (v : X) (i j : Fin m) : padWt K w m (mixTriple m v i j) = (1 - wLoad K w v) / ↑m ^ 2

theorem Nibble.Slack.padWt_nonneg {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (hw : ∀ (T : Finset X), 0 ≤ w T) (hload : ∀ (v : X), wLoad K w v ≤ 1) (U : Finset (Pad X m)) : 0 ≤ padWt K w m U

theorem Nibble.Slack.sum_padFam {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) (f : Finset (Pad X m) → ℝ) : ∑ U ∈ padFam K m, f U = ∑ T ∈ K, f (Finset.image Sum.inl T) + ∑ v : X, ∑ i : Fin m, ∑ j : Fin m, f (mixTriple m v i j)

The two halves of the padded family are disjoint, and both index maps are injective: so a sum over padFam splits into a sum over K and a sum over the mixed triples.

theorem Nibble.Slack.sum_wLoad {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (h3 : Hypergraph.IsUniform K 3) : ∑ x : X, wLoad K w x = 3 * ∑ T ∈ K, w T

Weighted handshake. For a 3-uniform hypergraph the loads add up to 3 times the total weight.

def Nibble.Slack.slackTotal {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) : ℝ

The total slack of the weighting.

Equations

• Nibble.Slack.slackTotal K w = ∑ v : X, (1 - Nibble.Slack.wLoad K w v)

theorem Nibble.Slack.padLoad_inl {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (hm : 0 < m) (v : X) : ∑ U ∈ padFam K m with Sum.inl v ∈ U, padWt K w m U = 1

theorem Nibble.Slack.padLoad_inr {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (hm : 0 < m) (d : Fin m × Bool) : ∑ U ∈ padFam K m with Sum.inr d ∈ U, padWt K w m U = slackTotal K w / ↑m

theorem Nibble.Slack.padFam_uniform {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) (hK : Hypergraph.IsUniform K 3) : Hypergraph.IsUniform (padFam K m) 3

theorem Nibble.Slack.slackTotal_nonneg {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (hload : ∀ (v : X), wLoad K w v ≤ 1) : 0 ≤ slackTotal K w

theorem Nibble.Slack.sum_padWt {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (hm : 0 < m) : ∑ U ∈ padFam K m, padWt K w m U = ∑ T ∈ K, w T + slackTotal K w

theorem Nibble.Slack.padCodeg_inl_inl {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) {v v' : X} (hvv : v ≠ v') : ∑ U ∈ padFam K m with Sum.inl v ∈ U ∧ Sum.inl v' ∈ U, padWt K w m U = ∑ T ∈ K with v ∈ T ∧ v' ∈ T, w T

theorem Nibble.Slack.padCodeg_inl_inr {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (hm : 0 < m) (v : X) (d : Fin m × Bool) : ∑ U ∈ padFam K m with Sum.inl v ∈ U ∧ Sum.inr d ∈ U, padWt K w m U = (1 - wLoad K w v) / ↑m

theorem Nibble.Slack.padCodeg_inr_inr {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (hm : 0 < m) (hload : ∀ (v : X), wLoad K w v ≤ 1) {d d' : Fin m × Bool} (hd : d ≠ d') : ∑ U ∈ padFam K m with Sum.inr d ∈ U ∧ Sum.inr d' ∈ U, padWt K w m U ≤ slackTotal K w / ↑m ^ 2

theorem Nibble.Slack.mem_padFam_of_toRight_empty {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) {U : Finset (Pad X m)} (hU : U ∈ padFam K m) (hR : U.toRight = ∅) : U.toLeft ∈ K ∧ U = Finset.image Sum.inl U.toLeft

A member of the padded family with no dummy vertices comes from K.

theorem Nibble.Slack.exists_left_dummy {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) {U : Finset (Pad X m)} (hU : U ∈ padFam K m) (hR : U.toRight ≠ ∅) : ∃ (i : Fin m), Sum.inr (i, false) ∈ U

A member of the padded family that does use a dummy contains a left dummy.

theorem Nibble.Slack.card_mixedPart_le {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) (hm : 0 < m) {M : Finset (Finset (Pad X m))} (hM : Hypergraph.IsMatching (padFam K m) M) : ↑{U ∈ M | U.toRight ≠ ∅}.card ≤ ↑m

A matching of the padded family uses at most m of the added triples: they are disjoint and each contains one of the m left dummies.

theorem Nibble.Slack.exists_matching_of_padMatching {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (m : ℕ) {M : Finset (Finset (Pad X m))} (hM : Hypergraph.IsMatching (padFam K m) M) : ∃ (M' : Finset (Finset X)), Hypergraph.IsMatching K M' ∧ ↑M'.card = ↑{U ∈ M | U.toRight = ∅}.card

The real part of a matching of the padded family projects to a matching of K of the same size.

theorem Nibble.Slack.padCodeg_comm {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (m : ℕ) (x z : Pad X m) : ∑ U ∈ padFam K m with x ∈ U ∧ z ∈ U, padWt K w m U = ∑ U ∈ padFam K m with z ∈ U ∧ x ∈ U, padWt K w m U

theorem Nibble.fracNibble_withSlack (β : ℝ) (hβ : 0 < β) : ∃ (γ : ℝ), 0 < γ ∧ ∀ {X : Type} [inst : Fintype X] [inst_1 : DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ), Hypergraph.IsUniform K 3 → (∀ (T : Finset X), 0 ≤ w T) → (∀ (v : X), Slack.wLoad K w v ≤ 1) → (∀ (x z : X), x ≠ z → ∑ T ∈ K with x ∈ T ∧ z ∈ T, w T ≤ γ) → 1 / γ ≤ ↑(Fintype.card X) - ∑ v : X, Slack.wLoad K w v → ∃ (M : Finset (Finset X)), Hypergraph.IsMatching K M ∧ (1 - β) * ∑ T ∈ K, w T - β * ↑(Fintype.card X) - 1 ≤ ↑M.card

The weighted nibble with slack. No near-perfection hypothesis: instead the weighting is required to leave a total slack S = |X| - ∑_v load v of at least 1/γ, and the conclusion loses β·|X| + 1.

Uniform weighted rounding with total slack

@[reducible, inline]

abbrev Nibble.SlackR.PadR (X : Type) (k m : ℕ) : Type

The padded vertex type: the real vertices together with k columns of m dummies.

Equations

• Nibble.SlackR.PadR X k m = (X ⊕ Fin k × Fin m)

def Nibble.SlackR.mixEdge {X : Type} [DecidableEq X] (k m : ℕ) (v : X) (i : Fin k → Fin m) : Finset (PadR X k m)

The added edge joining the real vertex v to the dummy i j of every column j.

Equations

• Nibble.SlackR.mixEdge k m v i = insert (Sum.inl v) (Finset.image (fun (j : Fin k) => Sum.inr (j, i j)) Finset.univ)

def Nibble.SlackR.padFamR {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) : Finset (Finset (PadR X k m))

The padded hypergraph: the image of K together with all the mixed edges.

Equations

• Nibble.SlackR.padFamR K k m = Finset.image (Finset.image Sum.inl) K ∪ Finset.image (fun (t : X × (Fin k → Fin m)) => Nibble.SlackR.mixEdge k m t.1 t.2) Finset.univ

noncomputable def Nibble.SlackR.padWtR {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) : Finset (PadR X k m) → ℝ

The padded weighting.

Equations

• Nibble.SlackR.padWtR K w k m U = if U.toRight = ∅ then w U.toLeft else (∑ v ∈ U.toLeft, (1 - Nibble.Slack.wLoad K w v)) / ↑m ^ k

Counting the dummy choices

theorem Nibble.SlackR.card_filter_eq_at (k m : ℕ) (j₀ : Fin k) (d : Fin m) : {i : Fin k → Fin m | i j₀ = d}.card = m ^ (k - 1)

The number of choice functions with a prescribed value in one column.

theorem Nibble.SlackR.card_filter_eq_at2 (k m : ℕ) {j₀ j₁ : Fin k} (hj : j₀ ≠ j₁) (d d' : Fin m) : {i : Fin k → Fin m | i j₀ = d ∧ i j₁ = d'}.card = m ^ (k - 2)

The number of choice functions with prescribed values in two distinct columns.

theorem Nibble.SlackR.sum_ite_at (k m : ℕ) (j₀ : Fin k) (d : Fin m) (c : ℝ) : (∑ i : Fin k → Fin m, if i j₀ = d then c else 0) = c * ↑m ^ (k - 1)

The sum of a constant over the choice functions with a prescribed value in one column.

theorem Nibble.SlackR.sum_ite_at2 (k m : ℕ) {j₀ j₁ : Fin k} (hj : j₀ ≠ j₁) (d d' : Fin m) (c : ℝ) : (∑ i : Fin k → Fin m, if i j₀ = d ∧ i j₁ = d' then c else 0) = c * ↑m ^ (k - 2)

The sum of a constant over the choice functions with prescribed values in two columns.

@[simp]

theorem Nibble.SlackR.toLeft_image_inl {X : Type} [DecidableEq X] (k m : ℕ) (T : Finset X) : (Finset.image Sum.inl T).toLeft = T

@[simp]

theorem Nibble.SlackR.toRight_image_inl {X : Type} [DecidableEq X] (k m : ℕ) (T : Finset X) : (Finset.image Sum.inl T).toRight = ∅

@[simp]

theorem Nibble.SlackR.mixEdge_toLeft {X : Type} [DecidableEq X] (k m : ℕ) (v : X) (i : Fin k → Fin m) : (mixEdge k m v i).toLeft = {v}

@[simp]

theorem Nibble.SlackR.mem_mixEdge_inl {X : Type} [DecidableEq X] (k m : ℕ) (v u : X) (i : Fin k → Fin m) : Sum.inl u ∈ mixEdge k m v i ↔ u = v

@[simp]

theorem Nibble.SlackR.mem_mixEdge_inr {X : Type} [DecidableEq X] (k m : ℕ) (v : X) (i : Fin k → Fin m) (j : Fin k) (d : Fin m) : Sum.inr (j, d) ∈ mixEdge k m v i ↔ i j = d

theorem Nibble.SlackR.mixEdge_toRight_nonempty {X : Type} [DecidableEq X] (k m : ℕ) (hk : 0 < k) (v : X) (i : Fin k → Fin m) : (mixEdge k m v i).toRight ≠ ∅

theorem Nibble.SlackR.mixEdge_card {X : Type} [DecidableEq X] (k m : ℕ) (v : X) (i : Fin k → Fin m) : (mixEdge k m v i).card = k + 1

theorem Nibble.SlackR.mixEdge_inj {X : Type} [DecidableEq X] (k m : ℕ) {v v' : X} {i i' : Fin k → Fin m} (h : mixEdge k m v i = mixEdge k m v' i') : v = v' ∧ i = i'

theorem Nibble.SlackR.padWtR_image_inl {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (T : Finset X) : padWtR K w k m (Finset.image Sum.inl T) = w T

theorem Nibble.SlackR.padWtR_mixEdge {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) (v : X) (i : Fin k → Fin m) : padWtR K w k m (mixEdge k m v i) = (1 - Slack.wLoad K w v) / ↑m ^ k

theorem Nibble.SlackR.padWtR_nonneg {X : Type} [DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hw : ∀ (T : Finset X), 0 ≤ w T) (hload : ∀ (v : X), Slack.wLoad K w v ≤ 1) (U : Finset (PadR X k m)) : 0 ≤ padWtR K w k m U

theorem Nibble.SlackR.sum_padFamR {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) (hk : 0 < k) (f : Finset (PadR X k m) → ℝ) : ∑ U ∈ padFamR K k m, f U = ∑ T ∈ K, f (Finset.image Sum.inl T) + ∑ v : X, ∑ i : Fin k → Fin m, f (mixEdge k m v i)

A sum over the padded family splits into a sum over K and a sum over the mixed edges.

theorem Nibble.SlackR.padFamR_uniform {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) (hK : Hypergraph.IsUniform K (k + 1)) : Hypergraph.IsUniform (padFamR K k m) (k + 1)

The number of dummy choice functions

theorem Nibble.SlackR.card_pi_fun (d m : ℕ) : ↑(Fintype.card (Fin d → Fin m)) = ↑m ^ d

The number of choice functions of one dummy per column, as a real number.

Loads, codegrees and matchings of the padded system

theorem Nibble.SlackR.pow_split_one (m k : ℕ) (hk : 0 < k) : ↑m ^ k = ↑m ^ (k - 1) * ↑m

theorem Nibble.SlackR.pow_split_two (m k : ℕ) (hk : 2 ≤ k) : ↑m ^ k = ↑m ^ (k - 2) * ↑m ^ 2

theorem Nibble.SlackR.sum_padWtR {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) (hm : 0 < m) : ∑ U ∈ padFamR K k m, padWtR K w k m U = ∑ T ∈ K, w T + Slack.slackTotal K w

The total weight of the padded system exceeds that of K by exactly the total slack.

theorem Nibble.SlackR.padLoad_inl {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) (hm : 0 < m) (v : X) : ∑ U ∈ padFamR K k m with Sum.inl v ∈ U, padWtR K w k m U = 1

Every real vertex has load exactly 1 in the padded system.

theorem Nibble.SlackR.padLoad_inr {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) (hm : 0 < m) (j : Fin k) (e : Fin m) : ∑ U ∈ padFamR K k m with Sum.inr (j, e) ∈ U, padWtR K w k m U = Slack.slackTotal K w / ↑m

Every dummy has load exactly S/m.

theorem Nibble.SlackR.padCodeg_inl_inl {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) {v v' : X} (hvv : v ≠ v') : ∑ U ∈ padFamR K k m with Sum.inl v ∈ U ∧ Sum.inl v' ∈ U, padWtR K w k m U = ∑ T ∈ K with v ∈ T ∧ v' ∈ T, w T

The weighted codegree of two real vertices is unchanged.

theorem Nibble.SlackR.padCodeg_inl_inr {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) (hm : 0 < m) (v : X) (j : Fin k) (e : Fin m) : ∑ U ∈ padFamR K k m with Sum.inl v ∈ U ∧ Sum.inr (j, e) ∈ U, padWtR K w k m U = (1 - Slack.wLoad K w v) / ↑m

The weighted codegree of a real vertex and a dummy.

theorem Nibble.SlackR.padCodeg_inr_inr {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (hk : 0 < k) (hm : 0 < m) (hload : ∀ (v : X), Slack.wLoad K w v ≤ 1) {d d' : Fin k × Fin m} (hd : d ≠ d') : ∑ U ∈ padFamR K k m with Sum.inr d ∈ U ∧ Sum.inr d' ∈ U, padWtR K w k m U ≤ Slack.slackTotal K w / ↑m ^ 2

The weighted codegree of two distinct dummies is at most S/m².

theorem Nibble.SlackR.padCodegR_comm {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) (k m : ℕ) (x z : PadR X k m) : ∑ U ∈ padFamR K k m with x ∈ U ∧ z ∈ U, padWtR K w k m U = ∑ U ∈ padFamR K k m with z ∈ U ∧ x ∈ U, padWtR K w k m U

theorem Nibble.SlackR.mem_padFamR_of_toRight_empty {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) (hk : 0 < k) {U : Finset (PadR X k m)} (hU : U ∈ padFamR K k m) (hR : U.toRight = ∅) : U.toLeft ∈ K ∧ U = Finset.image Sum.inl U.toLeft

A member of the padded family with no dummy vertices comes from K.

theorem Nibble.SlackR.exists_col_zero_dummy {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) (hk : 0 < k) {U : Finset (PadR X k m)} (hU : U ∈ padFamR K k m) (hR : U.toRight ≠ ∅) : ∃ (e : Fin m), Sum.inr (⟨0, hk⟩, e) ∈ U

A member of the padded family that uses a dummy contains a dummy of the first column.

theorem Nibble.SlackR.card_mixedPartR_le {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) (hk : 0 < k) (hm : 0 < m) {M : Finset (Finset (PadR X k m))} (hM : Hypergraph.IsMatching (padFamR K k m) M) : ↑{U ∈ M | U.toRight ≠ ∅}.card ≤ ↑m

A matching of the padded family uses at most m of the added edges.

theorem Nibble.SlackR.exists_matching_of_padMatchingR {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (k m : ℕ) (hk : 0 < k) {M : Finset (Finset (PadR X k m))} (hM : Hypergraph.IsMatching (padFamR K k m) M) : ∃ (M' : Finset (Finset X)), Hypergraph.IsMatching K M' ∧ ↑M'.card = ↑{U ∈ M | U.toRight = ∅}.card

The real part of a matching of the padded family projects to a matching of K of the same size.

theorem Nibble.SlackR.fracNibbleR_withSlack (k : ℕ) (hk : 0 < k) (β : ℝ) (hβ : 0 < β) : ∃ (γ : ℝ), 0 < γ ∧ ∀ {X : Type} [inst : Fintype X] [inst_1 : DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ), Hypergraph.IsUniform K (k + 1) → (∀ (T : Finset X), 0 ≤ w T) → (∀ (v : X), Slack.wLoad K w v ≤ 1) → (∀ (x z : X), x ≠ z → ∑ T ∈ K with x ∈ T ∧ z ∈ T, w T ≤ γ) → 1 / γ ≤ Slack.slackTotal K w → ∃ (M : Finset (Finset X)), Hypergraph.IsMatching K M ∧ (1 - β) * ∑ T ∈ K, w T - β * Slack.slackTotal K w - 1 ≤ ↑M.card

The weighted nibble with slack, in uniformity k+1. No near-perfection hypothesis: instead the weighting is required to leave a total slack of at least 1/γ, and the conclusion loses β·S + 1.

Weighted rounding for nonuniform hypergraphs with bounded edge size

@[reducible, inline]

abbrev Nibble.LEUnif.PadV (X : Type) (r m : ℕ) : Type

The padded vertex type: the real vertices together with r columns of m dummies.

Equations

• Nibble.LEUnif.PadV X r m = (X ⊕ Fin r × Fin m)

def Nibble.LEUnif.padEdgeD {X : Type} [DecidableEq X] (r m : ℕ) (T : Finset X) (i : Fin (r - T.card) → Fin m) : Finset (PadV X r m)

The padded edge of T for the dummy choice i: one dummy in each of the first r - #T columns.

Equations

• Nibble.LEUnif.padEdgeD r m T i = Finset.image Sum.inl T ∪ Finset.image (fun (j : Fin (r - T.card)) => Sum.inr (Fin.castLE ⋯ j, i j)) Finset.univ

def Nibble.LEUnif.padFamLE {X : Type} [DecidableEq X] (r m : ℕ) (K : Finset (Finset X)) : Finset (Finset (PadV X r m))

The padded family.

Equations

• Nibble.LEUnif.padFamLE r m K = K.biUnion fun (T : Finset X) => Finset.image (Nibble.LEUnif.padEdgeD r m T) Finset.univ

noncomputable def Nibble.LEUnif.padWtLE {X : Type} (r m : ℕ) (w : Finset X → ℝ) : Finset (PadV X r m) → ℝ

The padded weighting: the weight of T spread over its m^(r-#T) padded edges.

Equations

• Nibble.LEUnif.padWtLE r m w U = w U.toLeft / ↑m ^ (r - U.toLeft.card)

@[simp]

theorem Nibble.LEUnif.mem_padEdgeD_inl {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i : Fin (r - T.card) → Fin m} {x : X} : Sum.inl x ∈ padEdgeD r m T i ↔ x ∈ T

theorem Nibble.LEUnif.mem_padEdgeD_inr {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i : Fin (r - T.card) → Fin m} {j : Fin r} {e : Fin m} : Sum.inr (j, e) ∈ padEdgeD r m T i ↔ ∃ (j' : Fin (r - T.card)), ↑j' = ↑j ∧ i j' = e

@[simp]

theorem Nibble.LEUnif.padEdgeD_toLeft {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i : Fin (r - T.card) → Fin m} : (padEdgeD r m T i).toLeft = T

theorem Nibble.LEUnif.padEdgeD_inl_disj_inr {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i : Fin (r - T.card) → Fin m} : Disjoint (Finset.image Sum.inl T) (Finset.image (fun (j : Fin (r - T.card)) => Sum.inr (Fin.castLE ⋯ j, i j)) Finset.univ)

theorem Nibble.LEUnif.padEdgeD_card {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i : Fin (r - T.card) → Fin m} (hT : T.card ≤ r) : (padEdgeD r m T i).card = r

theorem Nibble.LEUnif.padEdgeD_inj_i {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i i' : Fin (r - T.card) → Fin m} (h : padEdgeD r m T i = padEdgeD r m T i') : i = i'

theorem Nibble.LEUnif.mem_padFamLE {X : Type} [DecidableEq X] {r m : ℕ} {K : Finset (Finset X)} {U : Finset (PadV X r m)} (hU : U ∈ padFamLE r m K) : ∃ (T : Finset X) (_ : T ∈ K) (i : Fin (r - T.card) → Fin m), U = padEdgeD r m T i

theorem Nibble.LEUnif.sum_padFamLE {X : Type} [DecidableEq X] {r m : ℕ} (K : Finset (Finset X)) (f : Finset (PadV X r m) → ℝ) : ∑ U ∈ padFamLE r m K, f U = ∑ T ∈ K, ∑ i : Fin (r - T.card) → Fin m, f (padEdgeD r m T i)

theorem Nibble.LEUnif.padWtLE_edge {X : Type} [DecidableEq X] {r m : ℕ} {T : Finset X} {i : Fin (r - T.card) → Fin m} (w : Finset X → ℝ) : padWtLE r m w (padEdgeD r m T i) = w T / ↑m ^ (r - T.card)

theorem Nibble.LEUnif.padWtLE_nonneg {X : Type} {r m : ℕ} (w : Finset X → ℝ) (hw : ∀ (T : Finset X), 0 ≤ w T) (U : Finset (PadV X r m)) : 0 ≤ padWtLE r m w U

theorem Nibble.LEUnif.padFamLE_uniform {X : Type} [DecidableEq X] {r m : ℕ} {K : Finset (Finset X)} (hK : ∀ T ∈ K, T.card ≤ r) : Hypergraph.IsUniform (padFamLE r m K) r

theorem Nibble.LEUnif.mul_pow_sub_one_div (x y : ℝ) (hy : 0 < y) (a : ℕ) (ha : 0 < a) : x * y ^ (a - 1) / y ^ a = x / y

theorem Nibble.LEUnif.mul_pow_sub_two_div (x y : ℝ) (hy : 0 < y) (a : ℕ) (ha : 2 ≤ a) : x * y ^ (a - 2) / y ^ a = x / y ^ 2

theorem Nibble.LEUnif.sum_col_one {m : ℕ} (hm : 0 < m) (x : ℝ) {d : ℕ} (j₀ : Fin d) (e : Fin m) : (∑ f : Fin d → Fin m, if f j₀ = e then x / ↑m ^ d else 0) = x / ↑m

One prescribed dummy: the weight x spread over m^d choices contributes x/m.

theorem Nibble.LEUnif.sum_col_two {m : ℕ} (hm : 0 < m) (x : ℝ) {d : ℕ} {j₀ j₁ : Fin d} (hj : j₀ ≠ j₁) (e e' : Fin m) : (∑ f : Fin d → Fin m, if f j₀ = e ∧ f j₁ = e' then x / ↑m ^ d else 0) = x / ↑m ^ 2

Two prescribed dummies in different columns contribute x/m².

theorem Nibble.LEUnif.sum_over_i {X : Type} {r m : ℕ} (hm : 0 < m) (w : Finset X → ℝ) (T : Finset X) : ∑ _i : Fin (r - T.card) → Fin m, w T / ↑m ^ (r - T.card) = w T

The sum of the padded weight over the padded edges of one T.

theorem Nibble.LEUnif.sum_padWtLE {X : Type} [DecidableEq X] {r m : ℕ} (hm : 0 < m) (K : Finset (Finset X)) (w : Finset X → ℝ) : ∑ U ∈ padFamLE r m K, padWtLE r m w U = ∑ T ∈ K, w T

theorem Nibble.LEUnif.padLoad_inl {X : Type} [DecidableEq X] {r m : ℕ} (hm : 0 < m) (K : Finset (Finset X)) (w : Finset X → ℝ) (v : X) : Slack.wLoad (padFamLE r m K) (padWtLE r m w) (Sum.inl v) = Slack.wLoad K w v

theorem Nibble.LEUnif.padLoad_inr {X : Type} [DecidableEq X] {r m : ℕ} (hm : 0 < m) (K : Finset (Finset X)) (w : Finset X → ℝ) (j : Fin r) (e : Fin m) : Slack.wLoad (padFamLE r m K) (padWtLE r m w) (Sum.inr (j, e)) = (∑ T ∈ K with ↑j < r - T.card, w T) / ↑m

theorem Nibble.LEUnif.padCodeg_inl_inl {X : Type} [DecidableEq X] {r m : ℕ} (K : Finset (Finset X)) (w : Finset X → ℝ) (hm : 0 < m) {v v' : X} : ∑ U ∈ padFamLE r m K with Sum.inl v ∈ U ∧ Sum.inl v' ∈ U, padWtLE r m w U = ∑ T ∈ K with v ∈ T ∧ v' ∈ T, w T

theorem Nibble.LEUnif.padCodeg_inl_inr {X : Type} [DecidableEq X] {r m : ℕ} (hm : 0 < m) (K : Finset (Finset X)) (w : Finset X → ℝ) (hw : ∀ (T : Finset X), 0 ≤ w T) (v : X) (j : Fin r) (e : Fin m) : ∑ U ∈ padFamLE r m K with Sum.inl v ∈ U ∧ Sum.inr (j, e) ∈ U, padWtLE r m w U ≤ Slack.wLoad K w v / ↑m

theorem Nibble.LEUnif.padCodeg_inr_inr {X : Type} [DecidableEq X] {r m : ℕ} (hm : 0 < m) (K : Finset (Finset X)) (w : Finset X → ℝ) (hw : ∀ (T : Finset X), 0 ≤ w T) {j j' : Fin r} {e e' : Fin m} (hne : (j, e) ≠ (j', e')) : ∑ U ∈ padFamLE r m K with Sum.inr (j, e) ∈ U ∧ Sum.inr (j', e') ∈ U, padWtLE r m w U ≤ (∑ T ∈ K, w T) / ↑m ^ 2

theorem Nibble.LEUnif.padCodegLE_comm {X : Type} [DecidableEq X] {r m : ℕ} (K : Finset (Finset X)) (w : Finset X → ℝ) (x z : PadV X r m) : ∑ U ∈ padFamLE r m K with x ∈ U ∧ z ∈ U, padWtLE r m w U = ∑ U ∈ padFamLE r m K with z ∈ U ∧ x ∈ U, padWtLE r m w U

theorem Nibble.LEUnif.sum_wLoad_eq {X : Type} [DecidableEq X] [Fintype X] (K : Finset (Finset X)) (w : Finset X → ℝ) : ∑ v : X, Slack.wLoad K w v = ∑ T ∈ K, ↑T.card * w T

Weighted handshake.

theorem Nibble.LEUnif.exists_matching_of_padMatchingLE {X : Type} [DecidableEq X] {r m : ℕ} {K : Finset (Finset X)} (hne : ∀ T ∈ K, T.Nonempty) {M : Finset (Finset (PadV X r m))} (hM : Hypergraph.IsMatching (padFamLE r m K) M) : ∃ (M' : Finset (Finset X)), Hypergraph.IsMatching K M' ∧ ↑M'.card = ↑M.card

A matching of the padded family projects to a matching of K of the same size.

theorem Nibble.fracNibble_leUniform (r : ℕ) (hr : 2 ≤ r) (β : ℝ) (hβ : 0 < β) : ∃ (γ : ℝ), 0 < γ ∧ ∃ (C : ℝ), 0 < C ∧ ∀ {X : Type} [inst : Fintype X] [inst_1 : DecidableEq X] (K : Finset (Finset X)) (w : Finset X → ℝ), (∀ T ∈ K, T.Nonempty ∧ T.card ≤ r) → (∀ (T : Finset X), 0 ≤ w T) → (∀ (v : X), Slack.wLoad K w v ≤ 1) → (∀ (x z : X), x ≠ z → ∑ T ∈ K with x ∈ T ∧ z ∈ T, w T ≤ γ) → ∃ (M : Finset (Finset X)), Hypergraph.IsMatching K M ∧ (1 - β) * ∑ T ∈ K, w T - β * ↑(Fintype.card X) - C ≤ ↑M.card

The weighted nibble for hypergraphs with edges of size at most r. For every accuracy β and every bound r on the edge size there are a codegree threshold γ and a constant C, depending on β and r alone, such that every weighting of a family of nonempty edges of size at most r with loads at most 1 and weighted codegrees at most γ admits a matching of size at least (1-β)·∑w − β·|X| − C.

theorem Nibble.boundedEdgeWeightedRounding_holds : Hypergraph.BoundedEdgeWeightedRounding

The proved theorem meets the independently stated bounded-edge interface.