Epsilon-loss recombination theorems

Bridge from arbitrary real-weighted collections to finite-uniform recombination, with an epsilon loss in the recombination inequality.

Auxiliary: M is nonneg, deficit helpers

theorem KaltonRoberts.M_nonneg_of_bound {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) : 0 ≤ M

theorem KaltonRoberts.deficit_nonneg_of_bound {U : Type u_1} (f : Finset U → ℝ) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (S : Finset U) : 0 ≤ deficit f M S

theorem KaltonRoberts.deficit_empty_eq {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) : deficit f M ∅ = M

Floor-based approximation of weighted collections

noncomputable def KaltonRoberts.WeightedCollection.floorCount {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (j : C.J) : ℕ

Floor count for index j when building a uniform family with N total indices.

Equations

• C.floorCount N j = ⌊↑N * C.weight j / C.totalWeight⌋₊

theorem KaltonRoberts.WeightedCollection.floorCount_le_frac {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (j : C.J) : ↑(C.floorCount N j) ≤ ↑N * C.weight j / C.totalWeight

Each floor count is at most the continuous fractional value.

theorem KaltonRoberts.WeightedCollection.floorCount_sum_le {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) : ∑ j : C.J, C.floorCount N j ≤ N

noncomputable def KaltonRoberts.WeightedCollection.emptyCount {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) : ℕ

The number of empty-set copies to pad up to N.

Equations

• C.emptyCount N = N - ∑ j : C.J, C.floorCount N j

theorem KaltonRoberts.WeightedCollection.emptyCount_le_card {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) : C.emptyCount N ≤ Fintype.card C.J

@[reducible, inline]

abbrev KaltonRoberts.WeightedCollection.ApproxIdx {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) : Type u_1

Approximate index type: sigma type for set copies plus empty copies.

Equations

• C.ApproxIdx N = ((j : C.J) × Fin (C.floorCount N j) ⊕ Fin (C.emptyCount N))

def KaltonRoberts.WeightedCollection.approxFam {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) : C.ApproxIdx N → Finset U

The approximation family: sigma part maps to sets, empty part maps to ∅.

Equations

• C.approxFam N (Sum.inl ⟨j, snd⟩) = C.sets j
• C.approxFam N (Sum.inr val) = ∅

theorem KaltonRoberts.WeightedCollection.approxIdx_card {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (h : ∑ j : C.J, C.floorCount N j ≤ N) : Fintype.card (C.ApproxIdx N) = N

theorem KaltonRoberts.WeightedCollection.approx_count {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (i : U) : {idx : C.ApproxIdx N | i ∈ C.approxFam N idx}.card = ∑ j : C.J with i ∈ C.sets j, C.floorCount N j

theorem KaltonRoberts.WeightedCollection.approx_freq_le {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (i : U) (hle : ∑ j : C.J, C.floorCount N j ≤ N) (hN : 0 < N) : ↑{idx : C.ApproxIdx N | i ∈ C.approxFam N idx}.card / ↑(Fintype.card (C.ApproxIdx N)) ≤ C.itemFreq i

theorem KaltonRoberts.WeightedCollection.approx_deficit_sum {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (f : Finset U → ℝ) (M : ℝ) : ∑ idx : C.ApproxIdx N, deficit f M (C.approxFam N idx) = ∑ j : C.J, ↑(C.floorCount N j) * deficit f M (C.sets j) + ↑(C.emptyCount N) * deficit f M ∅

theorem KaltonRoberts.WeightedCollection.approx_avgDeficit_le {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (N : ℕ) (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (D : ℝ) (hdeficit : C.avgDeficit f M ≤ D) (hle : ∑ j : C.J, C.floorCount N j ≤ N) (hN : 0 < N) : (∑ idx : C.ApproxIdx N, deficit f M (C.approxFam N idx)) / ↑(Fintype.card (C.ApproxIdx N)) ≤ D + ↑(Fintype.card C.J) * M / ↑N

Epsilon one-sided recombination

theorem KaltonRoberts.one_sided_recombination_core_eps {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) (_hα : 0 < ↑α_val) (C : WeightedCollection U) (hfreq : ∀ (i : U), C.itemFreq i ≤ ↑α_val) (D : ℝ) (hD : 0 ≤ D) (hdeficit : C.avgDeficit f M ≤ D) (ε : ℝ) (hε : 0 < ε) : ∃ (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

Lemma 3.2 (ε-version) One-sided recombination with epsilon loss. Bridges arbitrary real-weighted collections to the finite uniform theorem.

Epsilon two-sided recombination

theorem KaltonRoberts.two_sided_recombination_core_eps {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) (hα : 0 < ↑α_val) (C_def C_sur : WeightedCollection U) (hfreq_def : ∀ (i : U), C_def.itemFreq i ≤ ↑α_val) (hfreq_sur : ∀ (i : U), C_sur.itemFreq i ≤ ↑α_val) (D S_val : ℝ) (hD : 0 ≤ D) (hS : 0 ≤ S_val) (hdeficit : C_def.avgDeficit f M ≤ D) (hsurplus : C_sur.avgSurplus f M ≤ S_val) (ε : ℝ) (hε : 0 < ε) : ∃ (C'_def : WeightedCollection U) (C'_sur : WeightedCollection U) (D' : ℝ) (S' : ℝ), 0 ≤ D' ∧ 0 ≤ S' ∧ (∀ (i : U), C'_def.itemFreq i ≤ ↑α_val / ↑θ_val) ∧ (∀ (i : U), C'_sur.itemFreq i ≤ ↑α_val / ↑θ_val) ∧ C'_def.avgDeficit f M ≤ D' ∧ C'_sur.avgSurplus f M ≤ S' ∧ (1 - ↑θ_val) * M ≤ (D + S_val) / 2 + ε - ↑θ_val * ((D' + S') / 2) + 2 * ↑r_val - 1 - ↑θ_val

Lemma 3.3 (ε-version) Two-sided recombination with epsilon loss. Applies epsilon one-sided to deficit side and surplus side, then averages.