Pipeline from intersections to the final bound

Interfaces connecting weighted collections through mixed intersections and expander recombination to the final distance bound.

Mixed intersection construction

theorem KaltonRoberts.mixed_intersection_weighted {U : Type u_1} [DecidableEq U] [Finite U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (C : WeightedCollection U) (t : ℝ) (ht : 0 ≤ t) (ht1 : t ≤ 1) (hfreq : ∀ (i : U), C.itemFreq i ≤ t) (D : ℝ) (hD : 0 ≤ D) (hdeficit : C.avgDeficit f M ≤ D) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (τ_mix : ℝ) (hτ : 0 ≤ τ_mix) (hτ1 : τ_mix ≤ 1) : ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ_mix) * t ^ ℓ + τ_mix * t ^ (ℓ + 1)) ∧ C'.avgDeficit f M ≤ ↑ℓ * D + 2 * (↑ℓ - 1) + τ_mix * (D + 2)

Corollary 3.1 (Mixed intersections, deficit version).

theorem KaltonRoberts.mixed_intersection_weighted_surplus {U : Type u_1} [DecidableEq U] [Finite U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (C : WeightedCollection U) (t : ℝ) (ht : 0 ≤ t) (ht1 : t ≤ 1) (hfreq : ∀ (i : U), C.itemFreq i ≤ t) (S_val : ℝ) (hS : 0 ≤ S_val) (hsurplus : C.avgSurplus f M ≤ S_val) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (τ_mix : ℝ) (hτ : 0 ≤ τ_mix) (hτ1 : τ_mix ≤ 1) : ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ_mix) * t ^ ℓ + τ_mix * t ^ (ℓ + 1)) ∧ C'.avgSurplus f M ≤ ↑ℓ * S_val + 2 * (↑ℓ - 1) + τ_mix * (S_val + 2)

Corollary 3.1 (Mixed intersections, surplus version).

Expander existence for the four rows

The Pippenger construction and numerical certificates are in Pippenger.lean. The theorems are re-exported here for use in the spine proof.

theorem KaltonRoberts.expander_E₁ : StrongExpandersExist α₁ 4 (1 / 3)

theorem KaltonRoberts.expander_E₂ : StrongExpandersExist (3009 / 10000) 4 (4 / 7)

theorem KaltonRoberts.expander_E₃ : StrongExpandersExist α₂ 4 (2 / 7)

theorem KaltonRoberts.expander_E₄ : StrongExpandersExist (329 / 1250) 5 (5 / 11)

Normalization helpers

theorem KaltonRoberts.IsApproxAdditive_sub_additive {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (a : U → ℝ) : IsApproxAdditive (fun (S : Finset U) => f S - additiveFunction a S) 1

theorem KaltonRoberts.distToAdditive_sub_additive {U : Type u_1} (f : Finset U → ℝ) (a : U → ℝ) : (distToAdditive fun (S : Finset U) => f S - additiveFunction a S) = distToAdditive f

Negation helpers for the swap-to-small-q step

noncomputable def KaltonRoberts.DualCertificate.neg {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : DualCertificate (fun (S : Finset U) => -f S) M

Negated certificate: if cert is a DualCertificate for f with M, then negating lambda gives a DualCertificate for (-f) with M.

Equations

• cert.neg = { lam := fun (S : Finset U) => -cert.lam S, norm_one := ⋯, zero_marginals := ⋯, pos_support := ⋯, neg_support := ⋯ }

theorem KaltonRoberts.DualCertificate.neg_negMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.neg.negMass = cert.posMass

theorem KaltonRoberts.DualCertificate.neg_posMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.neg.posMass = cert.negMass

theorem KaltonRoberts.IsApproxAdditive_neg {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) : IsApproxAdditive (fun (S : Finset U) => -f S) 1

theorem KaltonRoberts.distToAdditive_neg {U : Type u_1} (f : Finset U → ℝ) : (distToAdditive fun (S : Finset U) => -f S) = distToAdditive f

Case 1 and Case 2 helpers for the spine theorem

theorem KaltonRoberts.best_approx_property {U : Type u_1} [Finite U] (g : Finset U → ℝ) (M : ℝ) (_hM_bound : ∀ (S : Finset U), |g S| ≤ M) (hM_eq : distToAdditive g = M) (a : U → ℝ) : ∃ (S : Finset U), |g S - additiveFunction a S| ≥ M

Helpers for the spine proofs

theorem KaltonRoberts.cert_posMass_pos {U : Type u_1} [DecidableEq U] [Fintype U] {g : Finset U → ℝ} {M : ℝ} (cert : DualCertificate g M) (hg : IsApproxAdditive g 1) (hM : 0 < M) (_hM_bound : ∀ (S : Finset U), |g S| ≤ M) : 0 < cert.posMass

theorem KaltonRoberts.cert_negMass_pos {U : Type u_1} [DecidableEq U] [Fintype U] {g : Finset U → ℝ} {M : ℝ} (cert : DualCertificate g M) (hg : IsApproxAdditive g 1) (hM : 0 < M) (hM_bound : ∀ (S : Finset U), |g S| ≤ M) : 0 < cert.negMass

theorem KaltonRoberts.g_univ_le_one {U : Type u_1} [DecidableEq U] [Fintype U] {g : Finset U → ℝ} {M : ℝ} (cert : DualCertificate g M) (hg : IsApproxAdditive g 1) (hM : 0 < M) (hM_bound : ∀ (S : Finset U), |g S| ≤ M) : |g Finset.univ| ≤ 1

theorem KaltonRoberts.spine_case1 {U : Type u_1} [DecidableEq U] [Fintype U] (g : Finset U → ℝ) (hg : IsApproxAdditive g 1) (M : ℝ) (hM_pos : 0 < M) (hM_bound : ∀ (S : Finset U), |g S| ≤ M) (cert : DualCertificate g M) (hq_le : cert.negMass ≤ ↑q₀) (hq_half : cert.negMass ≤ 1 / 2) (hmix : ∀ (C : WeightedCollection U) (t : ℝ), 0 ≤ t → t ≤ 1 → (∀ (i : U), C.itemFreq i ≤ t) → ∀ (D : ℝ), 0 ≤ D → C.avgDeficit g M ≤ D → ∀ (ℓ : ℕ), 1 ≤ ℓ → ∀ (τ : ℝ), 0 ≤ τ → τ ≤ 1 → ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ) * t ^ ℓ + τ * t ^ (ℓ + 1)) ∧ C'.avgDeficit g M ≤ ↑ℓ * D + 2 * (↑ℓ - 1) + τ * (D + 2)) (hrec1 : ∀ (α_v : ℚ) (r_v : ℕ) (θ_v : ℚ), 0 < ↑θ_v → ↑θ_v < 1 → StrongExpandersExist α_v r_v θ_v → ∀ (C : WeightedCollection U), (∀ (i : U), C.itemFreq i ≤ ↑α_v) → ∀ (D : ℝ), 0 ≤ D → C.avgDeficit g M ≤ D → ∃ (C' : WeightedCollection U) (D' : ℝ), 0 ≤ D' ∧ (∀ (i : U), C'.itemFreq i ≤ ↑α_v / ↑θ_v) ∧ C'.avgDeficit g M ≤ D' ∧ (1 - ↑θ_v) * M ≤ D - ↑θ_v * D' + 2 * ↑r_v - 1 - ↑θ_v) (hexp1 : StrongExpandersExist α₁ 4 (1 / 3)) (hexp2 : StrongExpandersExist (3009 / 10000) 4 (4 / 7)) : M ≤ ↑C₂

theorem KaltonRoberts.spine_case2 {U : Type u_1} [DecidableEq U] [Fintype U] (g : Finset U → ℝ) (hg : IsApproxAdditive g 1) (M : ℝ) (hM_pos : 0 < M) (hM_bound : ∀ (S : Finset U), |g S| ≤ M) (cert : DualCertificate g M) (hq_gt : ↑q₀ < cert.negMass) (hq_half : cert.negMass ≤ 1 / 2) (hmix : ∀ (C : WeightedCollection U) (t : ℝ), 0 ≤ t → t ≤ 1 → (∀ (i : U), C.itemFreq i ≤ t) → ∀ (D : ℝ), 0 ≤ D → C.avgDeficit g M ≤ D → ∀ (ℓ : ℕ), 1 ≤ ℓ → ∀ (τ : ℝ), 0 ≤ τ → τ ≤ 1 → ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ) * t ^ ℓ + τ * t ^ (ℓ + 1)) ∧ C'.avgDeficit g M ≤ ↑ℓ * D + 2 * (↑ℓ - 1) + τ * (D + 2)) (hmix_sur : ∀ (C : WeightedCollection U) (t : ℝ), 0 ≤ t → t ≤ 1 → (∀ (i : U), C.itemFreq i ≤ t) → ∀ (S_val : ℝ), 0 ≤ S_val → C.avgSurplus g M ≤ S_val → ∀ (ℓ : ℕ), 1 ≤ ℓ → ∀ (τ : ℝ), 0 ≤ τ → τ ≤ 1 → ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ) * t ^ ℓ + τ * t ^ (ℓ + 1)) ∧ C'.avgSurplus g M ≤ ↑ℓ * S_val + 2 * (↑ℓ - 1) + τ * (S_val + 2)) (hrec2 : ∀ (C_def C_sur : WeightedCollection U) (α_v : ℚ) (r_v : ℕ) (θ_v : ℚ), 0 < ↑θ_v → ↑θ_v < 1 → StrongExpandersExist α_v r_v θ_v → (∀ (i : U), C_def.itemFreq i ≤ ↑α_v) → (∀ (i : U), C_sur.itemFreq i ≤ ↑α_v) → ∀ (D S_val : ℝ), 0 ≤ D → 0 ≤ S_val → C_def.avgDeficit g M ≤ D → C_sur.avgSurplus g M ≤ S_val → ∃ (C'_def : WeightedCollection U) (C'_sur : WeightedCollection U) (D' : ℝ) (S' : ℝ), 0 ≤ D' ∧ 0 ≤ S' ∧ (∀ (i : U), C'_def.itemFreq i ≤ ↑α_v / ↑θ_v) ∧ (∀ (i : U), C'_sur.itemFreq i ≤ ↑α_v / ↑θ_v) ∧ C'_def.avgDeficit g M ≤ D' ∧ C'_sur.avgSurplus g M ≤ S' ∧ (1 - ↑θ_v) * M ≤ (D + S_val) / 2 - ↑θ_v * ((D' + S') / 2) + 2 * ↑r_v - 1 - ↑θ_v) (hexp3 : StrongExpandersExist α₂ 4 (2 / 7)) (hexp4 : StrongExpandersExist (329 / 1250) 5 (5 / 11)) : M ≤ ↑C₂