Pippenger expander construction

Row certificates and row-specific constructions for the probabilistic expander argument used in the Kalton-Roberts bound.

Row certificate structure

structure KaltonRoberts.PippengerRowCertificate (α : ℚ) (r : ℕ) (θ : ℚ) (c : ℕ) (δ : ℚ) : Prop

A PippengerRowCertificate captures exactly the hypotheses of Lemma 4.1 for one row of the expander table. Given parameters α r θ c δ, it asserts:

• Range conditions: 0 < α < θ < 1, 3 ≤ r, r < c, θ = r/c
• Tail bound: e² · θ^{1−r} · δ^{r−2} < 1/20
• Entropy negativity: Φ_{r,θ}(x) < 0 for all x ∈ [δ, α]

The paper uses c = r/θ. For the four rows:

• E₁: r = 4, θ = 1/3, c = 12
• E₂: r = 4, θ = 4/7, c = 7
• E₃: r = 4, θ = 2/7, c = 14
• E₄: r = 5, θ = 5/11, c = 11

• α_pos : 0 < α

  0 < α

• α_lt_θ : α < θ

  α < θ

• θ_lt_one : θ < 1

  θ < 1

• r_ge_three : 3 ≤ r

  3 ≤ r

• r_lt_c : r < c

  r < c

• θ_eq : θ = ↑r / ↑c

  θ = r / c (in ℚ)

• δ_pos : 0 < δ

  0 < δ

• δ_lt_α : δ < α

  δ < α

• tail_bound : Real.exp 2 * ↑θ ^ (1 - ↑r) * ↑δ ^ (↑r - 2) < 1 / 20

  Tail bound (real): e² · (θ : ℝ)^{1−r} · (δ : ℝ)^{r−2} < 1/20

• phi_neg (x : ℝ) : ↑δ ≤ x → x ≤ ↑α → Phi (↑r) (↑θ) x < 0

  Entropy negativity: Φ_{r,θ}(x) < 0 for all x ∈ [δ, α]

Tail bound proofs

theorem KaltonRoberts.tail_bound_real_E₁ : Real.exp 2 * ↑(1 / 3) ^ (1 - 4) * ↑(1 / 100) ^ (4 - 2) < 1 / 20

Tail bound for E₁: e² · (1/3)^{-3} · (1/100)^2 < 1/20

theorem KaltonRoberts.tail_bound_real_E₂ : Real.exp 2 * ↑(4 / 7) ^ (1 - 4) * ↑(1 / 100) ^ (4 - 2) < 1 / 20

Tail bound for E₂: e² · (4/7)^{-3} · (1/100)^2 < 1/20

theorem KaltonRoberts.tail_bound_real_E₃ : Real.exp 2 * ↑(2 / 7) ^ (1 - 4) * ↑(1 / 100) ^ (4 - 2) < 1 / 20

Tail bound for E₃: e² · (2/7)^{-3} · (1/100)^2 < 1/20

theorem KaltonRoberts.tail_bound_real_E₄ : Real.exp 2 * ↑(5 / 11) ^ (1 - 5) * ↑(1 / 100) ^ (5 - 2) < 1 / 20

Tail bound for E₄: e² · (5/11)^{-4} · (1/100)^3 < 1/20

Phi negativity on intervals

For each Pippenger row, the proof combines:

1. endpoint log certificates from LogBounds.lean,
2. derivative and convexity facts from PhiDeriv.lean, and
3. the endpoint-maximum property for convex functions.

Reference: Section 4 of the companion paper.

theorem KaltonRoberts.Phi_neg_E₁ (x : ℝ) : ↑(1 / 100) ≤ x → x ≤ ↑(1003 / 10000) → Phi (↑4) (↑(1 / 3)) x < 0

Phi negativity on [1/100, α₁] for E₁ (r=4, θ=1/3).

theorem KaltonRoberts.Phi_neg_E₂ (x : ℝ) : ↑(1 / 100) ≤ x → x ≤ ↑(3009 / 10000) → Phi (↑4) (↑(4 / 7)) x < 0

Phi negativity on [1/100, 3009/10000] for E₂ (r=4, θ=4/7).

theorem KaltonRoberts.Phi_neg_E₃ (x : ℝ) : ↑(1 / 100) ≤ x → x ≤ ↑(47 / 625) → Phi (↑4) (↑(2 / 7)) x < 0

Phi negativity on [1/100, 47/625] for E₃ (r=4, θ=2/7).

theorem KaltonRoberts.Phi_neg_E₄ (x : ℝ) : ↑(1 / 100) ≤ x → x ≤ ↑(329 / 1250) → Phi (↑5) (↑(5 / 11)) x < 0

Phi negativity on [1/100, 329/1250] for E₄ (r=5, θ=5/11).

theorem KaltonRoberts.Phi_margin_E₁ (x : ℝ) : 1 / 100 ≤ x → x ≤ 1003 / 10000 → Phi 4 (1 / 3) x ≤ -1 / 1000

theorem KaltonRoberts.Phi_margin_E₂ (x : ℝ) : 1 / 100 ≤ x → x ≤ 3009 / 10000 → Phi 4 (4 / 7) x ≤ -1 / 1000

theorem KaltonRoberts.Phi_margin_E₃ (x : ℝ) : 1 / 100 ≤ x → x ≤ 47 / 625 → Phi 4 (2 / 7) x ≤ -1 / 1000

theorem KaltonRoberts.Phi_margin_E₄ (x : ℝ) : 1 / 100 ≤ x → x ≤ 329 / 1250 → Phi 5 (5 / 11) x ≤ -1 / 1000

Row certificates

theorem KaltonRoberts.row_certificate_E₁ : PippengerRowCertificate (1003 / 10000) 4 (1 / 3) 12 (1 / 100)

Row certificate for E₁: α = 1003/10000, r = 4, θ = 1/3, c = 12, δ = 1/100.

theorem KaltonRoberts.row_certificate_E₂ : PippengerRowCertificate (3009 / 10000) 4 (4 / 7) 7 (1 / 100)

Row certificate for E₂: α = 3009/10000, r = 4, θ = 4/7, c = 7, δ = 1/100.

theorem KaltonRoberts.row_certificate_E₃ : PippengerRowCertificate (47 / 625) 4 (2 / 7) 14 (1 / 100)

Row certificate for E₃: α = 47/625, r = 4, θ = 2/7, c = 14, δ = 1/100.

theorem KaltonRoberts.row_certificate_E₄ : PippengerRowCertificate (329 / 1250) 5 (5 / 11) 11 (1 / 100)

Row certificate for E₄: α = 329/1250, r = 5, θ = 5/11, c = 11, δ = 1/100.

Row-specific bad-ratio estimates

theorem KaltonRoberts.tail_bound_E₁_simplified : Real.exp 2 * 27 * (1 / 100) ^ 2 < 1 / 20

theorem KaltonRoberts.small_term_E₁ (N L m : ℕ) (hN : 0 < N) (hm : 0 < m) (hmN : m ≤ N) (hmL : m ≤ L) (hNL : 4 * N = 12 * L) (hLreal : ↑L = 1 / 3 * ↑N) (hsmall : ↑m / ↑N ≤ 1 / 100) : ↑(N.choose m) * ↑(L.choose m) * ↑((12 * m).choose (4 * m)) / ↑((4 * N).choose (4 * m)) ≤ (1 / 20) ^ m

theorem KaltonRoberts.bad_ratio_sum_E₁_core (t : ℕ) (ht : 0 < t) (hdec : 50 * ↑(15000 * t) ^ 2 * Real.exp (-(1 / 500) * ↑(15000 * t)) < 1 / 2) : ∑ m ∈ Finset.Icc 1 (3009 * t), ↑((30000 * t).choose m) * ↑((10000 * t).choose m) * (↑((12 * m).choose (4 * m)) / ↑((4 * (30000 * t)).choose (4 * m))) < 1

theorem KaltonRoberts.tail_bound_E₂_simplified : Real.exp 2 * (7 / 4) ^ 3 * (1 / 100) ^ 2 < 1 / 20

theorem KaltonRoberts.small_term_E₂ (N L m : ℕ) (hN : 0 < N) (hm : 0 < m) (hmN : m ≤ N) (hmL : m ≤ L) (hNL : 4 * N = 7 * L) (hLreal : ↑L = 4 / 7 * ↑N) (hsmall : ↑m / ↑N ≤ 1 / 100) : ↑(N.choose m) * ↑(L.choose m) * ↑((7 * m).choose (4 * m)) / ↑((4 * N).choose (4 * m)) ≤ (1 / 20) ^ m

theorem KaltonRoberts.bad_ratio_sum_E₂_core (t : ℕ) (ht : 0 < t) (hdec : 50 * ↑(35000 * t) ^ 2 * Real.exp (-(1 / 500) * ↑(35000 * t)) < 1 / 2) : ∑ m ∈ Finset.Icc 1 (21063 * t), ↑((70000 * t).choose m) * ↑((40000 * t).choose m) * (↑((7 * m).choose (4 * m)) / ↑((4 * (70000 * t)).choose (4 * m))) < 1

theorem KaltonRoberts.tail_bound_E₃_simplified : Real.exp 2 * (7 / 2) ^ 3 * (1 / 100) ^ 2 < 1 / 20

theorem KaltonRoberts.small_term_E₃ (N L m : ℕ) (hN : 0 < N) (hm : 0 < m) (hmN : m ≤ N) (hmL : m ≤ L) (hNL : 4 * N = 14 * L) (hLreal : ↑L = 2 / 7 * ↑N) (hsmall : ↑m / ↑N ≤ 1 / 100) : ↑(N.choose m) * ↑(L.choose m) * ↑((14 * m).choose (4 * m)) / ↑((4 * N).choose (4 * m)) ≤ (1 / 20) ^ m

theorem KaltonRoberts.bad_ratio_sum_E₃_core (t : ℕ) (ht : 0 < t) (hdec : 50 * ↑(8750 * t) ^ 2 * Real.exp (-(1 / 500) * ↑(8750 * t)) < 1 / 2) : ∑ m ∈ Finset.Icc 1 (1316 * t), ↑((17500 * t).choose m) * ↑((5000 * t).choose m) * (↑((14 * m).choose (4 * m)) / ↑((4 * (17500 * t)).choose (4 * m))) < 1

theorem KaltonRoberts.tail_bound_E₄_simplified : Real.exp 2 * (11 / 5) ^ 4 * (1 / 100) ^ 3 < 1 / 20

theorem KaltonRoberts.small_term_E₄ (N L m : ℕ) (hN : 0 < N) (hm : 0 < m) (hmN : m ≤ N) (hmL : m ≤ L) (hNL : 5 * N = 11 * L) (hLreal : ↑L = 5 / 11 * ↑N) (hsmall : ↑m / ↑N ≤ 1 / 100) : ↑(N.choose m) * ↑(L.choose m) * ↑((11 * m).choose (5 * m)) / ↑((5 * N).choose (5 * m)) ≤ (1 / 20) ^ m

theorem KaltonRoberts.bad_ratio_sum_E₄_core (t : ℕ) (ht : 0 < t) (hdec : 50 * ↑(13750 * t) ^ 2 * Real.exp (-(1 / 500) * ↑(13750 * t)) < 1 / 2) : ∑ m ∈ Finset.Icc 1 (7238 * t), ↑((27500 * t).choose m) * ↑((12500 * t).choose m) * (↑((11 * m).choose (5 * m)) / ↑((5 * (27500 * t)).choose (5 * m))) < 1

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

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

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

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

Combined expander existence

theorem KaltonRoberts.pippenger_required_expanders : StrongExpandersExist α₁ 4 (1 / 3) ∧ StrongExpandersExist (3009 / 10000) 4 (4 / 7) ∧ StrongExpandersExist α₂ 4 (2 / 7) ∧ StrongExpandersExist (329 / 1250) 5 (5 / 11)

The four expander existence claims, proved by row-specific Pippenger constructions.