Documentation

LeanPool.KaltonRoberts.PipelineEps

Epsilon pipeline #

Spine theorems with epsilon-loss recombination and the final exact C₂ bound.

Case 1 spine with epsilon recombination #

source
theorem KaltonRoberts.spine_case1_eps {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_eps : ∀ (α_v : ℚ) (r_v : ℕ) (θ_v : ℚ), 0 < ↑θ_v → ↑θ_v < 1 → StrongExpandersExist α_v r_v θ_v → 0 < r_v → 0 < ↑α_v → ∀ (C : WeightedCollection U), (∀ (i : U), C.itemFreq i ≤ ↑α_v) → ∀ (D : ℝ), 0 ≤ D → C.avgDeficit g M ≤ D → ∀ (ε : ℝ), 0 < ε → ∃ (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)) (ε : ℝ) (hε : 0 < ε) :
M ≤ ↑C₂ + 2 * ε

Case 1 spine with epsilon recombination. Same as spine_case1 but with epsilon one-sided recombination. Proves M ≤ C₂ + 2 * ε.

Case 2 spine with epsilon recombination #

source
theorem KaltonRoberts.spine_case2_eps {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_eps : ∀ (C_def C_sur : WeightedCollection U) (α_v : ℚ) (r_v : ℕ) (θ_v : ℚ), 0 < ↑θ_v → ↑θ_v < 1 → StrongExpandersExist α_v r_v θ_v → 0 < r_v → 0 < ↑α_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 → ∀ (ε : ℝ), 0 < ε → ∃ (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)) (ε : ℝ) (hε : 0 < ε) :
M ≤ ↑C₂ + 2 * ε

Case 2 spine with epsilon recombination. Same as spine_case2 but with epsilon two-sided recombination. Proves M ≤ C₂ + 2 * ε.

The Section 5 spine theorem (epsilon version) #

source
theorem KaltonRoberts.distToAdditive_le_C₂_from_pipeline {U : Type u_1} [DecidableEq U] [Finite U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (hnorm : ∃ (a : U → ℝ), ∀ (S : Finset U), |f S - additiveFunction a S| ≤ distToAdditive f) (hmix : ∀ (g : Finset U → ℝ), IsApproxAdditive g 1 → ∀ (M : ℝ), (∀ (S : Finset U), |g S| ≤ M) → ∀ (C : WeightedCollection U) (t : ℝ), 0 ≤ t → t ≤ 1 → (∀ (i : U), C.itemFreq i ≤ t) → ∀ (D : ℝ), 0 ≤ D → C.avgDeficit g M ≤ D → ∀ (ℓ : ℕ), 1 ≤ ℓ → ∀ (τ_mix : ℝ), 0 ≤ τ_mix → τ_mix ≤ 1 → ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ_mix) * t ^ ℓ + τ_mix * t ^ (ℓ + 1)) ∧ C'.avgDeficit g M ≤ ↑ℓ * D + 2 * (↑ℓ - 1) + τ_mix * (D + 2)) (hmix_sur : ∀ (g : Finset U → ℝ), IsApproxAdditive g 1 → ∀ (M : ℝ), (∀ (S : Finset U), |g S| ≤ M) → ∀ (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 ≤ ℓ → ∀ (τ_mix : ℝ), 0 ≤ τ_mix → τ_mix ≤ 1 → ∃ (C' : WeightedCollection U), (∀ (i : U), C'.itemFreq i ≤ (1 - τ_mix) * t ^ ℓ + τ_mix * t ^ (ℓ + 1)) ∧ C'.avgSurplus g M ≤ ↑ℓ * S_val + 2 * (↑ℓ - 1) + τ_mix * (S_val + 2)) (hrec1_eps : ∀ (g : Finset U → ℝ), IsApproxAdditive g 1 → ∀ (M : ℝ), (∀ (S : Finset U), |g S| ≤ M) → ∀ (α_v : ℚ) (r_v : ℕ) (θ_v : ℚ), 0 < ↑θ_v → ↑θ_v < 1 → StrongExpandersExist α_v r_v θ_v → 0 < r_v → 0 < ↑α_v → ∀ (C : WeightedCollection U), (∀ (i : U), C.itemFreq i ≤ ↑α_v) → ∀ (D : ℝ), 0 ≤ D → C.avgDeficit g M ≤ D → ∀ (ε : ℝ), 0 < ε → ∃ (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) (hrec2_eps : ∀ (g : Finset U → ℝ), IsApproxAdditive g 1 → ∀ (M : ℝ), (∀ (S : Finset U), |g S| ≤ M) → ∀ (α_v : ℚ) (r_v : ℕ) (θ_v : ℚ), 0 < ↑θ_v → ↑θ_v < 1 → StrongExpandersExist α_v r_v θ_v → 0 < r_v → 0 < ↑α_v → ∀ (C_def C_sur : WeightedCollection U), (∀ (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 → ∀ (ε : ℝ), 0 < ε → ∃ (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) (hexp1 : StrongExpandersExist α₁ 4 (1 / 3)) (hexp2 : StrongExpandersExist (3009 / 10000) 4 (4 / 7)) (hexp3 : StrongExpandersExist α₂ 4 (2 / 7)) (hexp4 : StrongExpandersExist (329 / 1250) 5 (5 / 11)) :
distToAdditive f ≤ ↑C₂

Spine theorem (epsilon version): distToAdditive f ≤ C₂ assuming all pipeline components with epsilon recombination.

Uses the real-analysis principle: if ∀ ε > 0, x ≤ y + ε, then x ≤ y.

Reference: Section 5 of the companion paper.