One-sided recombination

Witness-level one-sided recombination theorem for approximate additive functions.

Approximate-additivity partition lemmas

theorem KaltonRoberts.approx_additive_finset_partition_lower {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (n : ℕ) (hn : 1 ≤ n) (pieces : Fin n → Finset U) (hpw : ∀ (i j : Fin n), i ≠ j → Disjoint (pieces i) (pieces j)) (A : Finset U) (hunion : A = Finset.univ.biUnion pieces) : f A ≥ ∑ i : Fin n, f (pieces i) - (↑n - 1)

If f is 1-additive and pieces : Fin n → Finset U are pairwise disjoint with union A, then f(A) ≥ ∑ f(pieces) - (n - 1).

theorem KaltonRoberts.approx_additive_finset_partition_upper {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (n : ℕ) (hn : 1 ≤ n) (pieces : Fin n → Finset U) (hpw : ∀ (i j : Fin n), i ≠ j → Disjoint (pieces i) (pieces j)) (A : Finset U) (hunion : A = Finset.univ.biUnion pieces) : ∑ i : Fin n, f (pieces i) ≤ f A + (↑n - 1)

If f is 1-additive and pieces : Fin n → Finset U are pairwise disjoint with union A, then ∑ f(pieces) ≤ f(A) + (n - 1).

theorem KaltonRoberts.approx_additive_finset_partition_sum_lower {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (n : ℕ) (hn : 1 ≤ n) (pieces : Fin n → Finset U) (hpw : ∀ (i j : Fin n), i ≠ j → Disjoint (pieces i) (pieces j)) (A : Finset U) (hunion : A = Finset.univ.biUnion pieces) : ∑ i : Fin n, f (pieces i) ≥ f A - (↑n - 1)

Hall matching from expansion

theorem KaltonRoberts.hall_matching_from_expansion {V : Type u_2} {W : Type u_3} [_hV : Finite V] [_hW : Finite W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (A : Finset V) (hA : A.card ≤ threshold) : ∃ (match_fn : ↥A → W), Function.Injective match_fn ∧ ∀ (x : ↥A), match_fn x ∈ edgeNeighbors edge ↑x

From an expander's expansion property, derive Hall's matching for any subset of left vertices of size at most the expansion threshold.

Recombination construction

def KaltonRoberts.sourceVertices {U : Type u_1} [DecidableEq U] {V : Type u_2} [Fintype V] (C : V → Finset U) (i : U) : Finset V

For each item i, the set of source vertices containing it.

Equations

• KaltonRoberts.sourceVertices C i = {v : V | i ∈ C v}

noncomputable def KaltonRoberts.perItemMatch {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (i : U) : ↥(sourceVertices C i) → W

Per-item Hall matching: for each item i, an injective map from source vertices containing i into W, landing in the edge-neighbor set.

Equations

• KaltonRoberts.perItemMatch edge C threshold hexp hfreq i = ⋯.choose

theorem KaltonRoberts.perItemMatch_injective {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (i : U) : Function.Injective (perItemMatch edge C threshold hexp hfreq i)

theorem KaltonRoberts.perItemMatch_mem_neighbors {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (i : U) (x : ↥(sourceVertices C i)) : perItemMatch edge C threshold hexp hfreq i x ∈ edgeNeighbors edge ↑x

noncomputable def KaltonRoberts.assignLabel {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (v : V) (i : U) (hi : i ∈ C v) : Fin r

For each source vertex v and item i ∈ C v, choose an edge label e : Fin r such that edge v e equals the matched target of (v, i).

Equations

• KaltonRoberts.assignLabel edge C threshold hexp hfreq v i hi = ⋯.choose

theorem KaltonRoberts.assignLabel_spec {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (v : V) (i : U) (hi : i ∈ C v) : edge v (assignLabel edge C threshold hexp hfreq v i hi) = perItemMatch edge C threshold hexp hfreq i ⟨v, ⋯⟩

noncomputable def KaltonRoberts.edgePiece {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (v : V) (e : Fin r) : Finset U

Edge piece: for each v : V and e : Fin r, the subset of C v whose assigned edge label is e.

Equations

• KaltonRoberts.edgePiece edge C threshold hexp hfreq v e = {i ∈ C v | ∃ (hi : i ∈ C v), KaltonRoberts.assignLabel edge C threshold hexp hfreq v i hi = e}

noncomputable def KaltonRoberts.targetSet {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (w : W) : Finset U

Target set: for each w : W, the union of all edge pieces arriving at w.

Equations

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

Properties of the construction

theorem KaltonRoberts.edgePiece_union {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (v : V) : C v = Finset.univ.biUnion fun (e : Fin r) => edgePiece edge C threshold hexp hfreq v e

theorem KaltonRoberts.edgePiece_pairwise_disjoint {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (v : V) (e₁ e₂ : Fin r) (he : e₁ ≠ e₂) : Disjoint (edgePiece edge C threshold hexp hfreq v e₁) (edgePiece edge C threshold hexp hfreq v e₂)

theorem KaltonRoberts.targetSet_freq_source_count_bound {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (i : U) : {w : W | i ∈ targetSet edge C threshold hexp hfreq w}.card ≤ (sourceVertices C i).card

theorem KaltonRoberts.targetSet_freq_bound {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (C : V → Finset U) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) (i : U) : {w : W | i ∈ targetSet edge C threshold hexp hfreq w}.card ≤ threshold

theorem KaltonRoberts.recombination_source_target_ineq {U : Type u_1} [DecidableEq U] {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (hcov : ∀ (w : W), ∃ (v : V) (e : Fin r), edge v e = w) (hr : 0 < r) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (_M : ℝ) (C : V → Finset U) (hfreq : ∀ (i : U), (sourceVertices C i).card ≤ threshold) : ∑ v : V, f (C v) ≤ ∑ w : W, f (targetSet edge C threshold hexp hfreq w) + 2 * ↑r * ↑(Fintype.card V) - ↑(Fintype.card V) - ↑(Fintype.card W)

One-sided recombination: witness-level core

theorem KaltonRoberts.one_sided_recombination_witness_core {U : Type u_1} [DecidableEq U] {V : Type u_4} {W : Type u_5} [Fintype V] [Fintype W] [DecidableEq W] {r : ℕ} (hr : 0 < r) (edge : V → Fin r → W) (hcov : ∀ (w : W), ∃ (v : V) (e : Fin r), edge v e = w) (threshold : ℕ) (hexp : ∀ (S : Finset V), S.card ≤ threshold → (S.biUnion fun (v : V) => edgeNeighbors edge v).card ≥ S.card) (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (C : V → Finset U) (hfreq : ∀ (i : U), {v : V | i ∈ C v}.card ≤ threshold) (D : ℝ) (_hD : 0 ≤ D) (havg_def : (∑ v : V, deficit f M (C v)) / ↑(Fintype.card V) ≤ D) (hN : 0 < ↑(Fintype.card V)) (hL : 0 < ↑(Fintype.card W)) : ∃ (T : W → Finset U) (D' : ℝ), 0 ≤ D' ∧ (∀ (i : U), {w : W | i ∈ T w}.card ≤ {v : V | i ∈ C v}.card) ∧ (∀ (i : U), {w : W | i ∈ T w}.card ≤ threshold) ∧ (∑ w : W, deficit f M (T w)) / ↑(Fintype.card W) ≤ D' ∧ (1 - ↑(Fintype.card W) / ↑(Fintype.card V)) * M ≤ D - ↑(Fintype.card W) / ↑(Fintype.card V) * D' + 2 * ↑r - 1 - ↑(Fintype.card W) / ↑(Fintype.card V)

one_sided_recombination_witness_core is the concrete finite-expander version of Lemma 3.2. The lifted uniform and epsilon-weighted versions used by the main theorem live in UniformRecombination.lean and EpsilonRecombination.lean.