Finite-uniform recombination #

Finite-uniform version of the one-sided recombination theorem, producing a target weighted collection via expander recombination.

Uniform labeling helpers #

theorem KaltonRoberts.exists_uniform_labeling (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (hdvd : m ∣ n) :

∃ (f : Fin n → Fin m), Function.Surjective f ∧ ∀ (j : Fin m), {i : Fin n | f i = j}.card = n / m

For m ∣ n with 0 < n and 0 < m, the function i ↦ i % m maps Fin n to Fin m with each fiber having exactly n / m elements.

∃ (f : A → B), Function.Surjective f ∧ ∀ (j : B), {i : A | f i = j}.card = Fintype.card A / Fintype.card B

theorem KaltonRoberts.exists_large_admissible_multiple (step d : ℕ) (hstep : 0 < step) (hd : 0 < d) (N : ℕ) :

∃ (k : ℕ), N ≤ k ∧ step ∣ k ∧ d ∣ 2 * k

For any positive integers step and d, there exist arbitrarily large multiples of step such that d ∣ 2 * k.

theorem KaltonRoberts.uniform_duplication_source_count' {U : Type u_1} [DecidableEq U] {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] [DecidableEq B] (lab : A → B) (hfiber : ∀ (j : B), {i : A | lab i = j}.card = Fintype.card A / Fintype.card B) (C : B → Finset U) (i : U) :

{v : A | i ∈ C (lab v)}.card = {j : B | i ∈ C j}.card * (Fintype.card A / Fintype.card B)

theorem KaltonRoberts.uniform_duplication_sum {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] [DecidableEq B] (lab : A → B) (hfiber : ∀ (j : B), {i : A | lab i = j}.card = Fintype.card A / Fintype.card B) (g : B → ℝ) :

∑ v : A, g (lab v) = ↑(Fintype.card A / Fintype.card B) * ∑ j : B, g j

theorem KaltonRoberts.expander_ratio_eq_theta {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] {θ : ℚ} {k : ℕ} (hk : 0 < k) (hV : Fintype.card V = 2 * k) (hW : ↑(Fintype.card W) = 2 * θ * ↑k) :

theorem KaltonRoberts.one_sided_recombination_uniform_core {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (α_val : ℚ) (r_val : ℕ) (θ_val : ℚ) (hθ : 0 < ↑θ_val) (_hθ1 : ↑θ_val < 1) (hexp : StrongExpandersExist α_val r_val θ_val) (hr : 0 < r_val) {I : Type u_2} [Fintype I] (hI : 0 < Fintype.card I) (C : I → Finset U) (hfreq : ∀ (i : U), ↑{j : I | i ∈ C j}.card / ↑(Fintype.card I) ≤ ↑α_val) (D : ℝ) (hD : 0 ≤ D) (havg_def : (∑ j : I, deficit f M (C j)) / ↑(Fintype.card I) ≤ D) :

∃ (C' : WeightedCollection U) (D' : ℝ), 0 ≤ D' ∧ (∀ (i : U), C'.itemFreq i ≤ ↑α_val / ↑θ_val) ∧ C'.avgDeficit f M ≤ D' ∧ (1 - ↑θ_val) * M ≤ D - ↑θ_val * D' + 2 * ↑r_val - 1 - ↑θ_val