Pippenger expander construction proof

Probabilistic counting argument proving existence of expanders for the rows needed by the Kalton-Roberts bound.

Counting constrained permutations

theorem KaltonRoberts.card_perm_constrained_zero (n t : ℕ) (_ht : t ≤ n) : Fintype.card { σ : Equiv.Perm (Fin n) // ∀ (i : Fin n), ↑i < 0 → ↑(σ i) < t } = n.factorial

theorem KaltonRoberts.card_perm_constrained_step (n s t : ℕ) (hs : s < t) (ht : t ≤ n) : Fintype.card { σ : Equiv.Perm (Fin n) // ∀ (i : Fin n), ↑i < s + 1 → ↑(σ i) < t } * (n - s) = Fintype.card { σ : Equiv.Perm (Fin n) // ∀ (i : Fin n), ↑i < s → ↑(σ i) < t } * (t - s)

theorem KaltonRoberts.card_perm_constrained (n s t : ℕ) (hs : s ≤ t) (ht : t ≤ n) : Fintype.card { σ : Equiv.Perm (Fin n) // ∀ (i : Fin n), ↑i < s → ↑(σ i) < t } = t.descFactorial s * (n - s).factorial

The number of permutations of Fin n that map the first s elements into {0, …, t-1} is t.descFactorial s * (n - s)!.

Binomial coefficient bounds

theorem KaltonRoberts.choose_le_exp_pow (n k : ℕ) (hk : 0 < k) (_hkn : k ≤ n) : ↑(n.choose k) ≤ (Real.exp 1 * ↑n / ↑k) ^ k

theorem KaltonRoberts.choose_le_exp_h_entropy (n k : ℕ) (hk : 0 < k) (hkn : k < n) : ↑(n.choose k) ≤ Real.exp (hEntropy ↑n ↑k)

theorem KaltonRoberts.choose_ge_exp_h_entropy_div (n k : ℕ) (hk : 0 < k) (hkn : k < n) : Real.exp (hEntropy ↑n ↑k) / (↑n + 1) ≤ ↑(n.choose k)

Descending factorial ratio bound

theorem KaltonRoberts.desc_fact_ratio_le (a b k : ℕ) (hab : a ≤ b) (hka : k ≤ a) : ↑(a.descFactorial k) / ↑(b.descFactorial k) ≤ (↑a / ↑b) ^ k

Geometric and exponential tail bounds

theorem KaltonRoberts.geom_sum_le (d : ℕ) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) : ∑ i ∈ Finset.range d, q ^ (i + 1) ≤ q / (1 - q)

theorem KaltonRoberts.sum_Icc_one_pow_le_geom (D : ℕ) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) : ∑ m ∈ Finset.Icc 1 D, q ^ m ≤ q / (1 - q)

theorem KaltonRoberts.bad_sum_split (A D N : ℕ) (T : ℕ → ℝ) (q B : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) (hB0 : 0 ≤ B) (hcard_N : (Finset.Icc 1 A).card ≤ N) (hsmall : ∀ m ∈ Finset.Icc 1 A, m ≤ D → T m ≤ q ^ m) (hmid : ∀ m ∈ Finset.Icc 1 A, D < m → T m ≤ B) : ∑ m ∈ Finset.Icc 1 A, T m ≤ q / (1 - q) + ↑N * B

theorem KaltonRoberts.exp_decay_beats_poly (η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, ↑N ^ 2 * Real.exp (-η * ↑N) < 1 / 2

theorem KaltonRoberts.exp_decay_beats_poly_const (C η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, C * ↑N ^ 2 * Real.exp (-η * ↑N) < 1 / 2

Entropy bounds for Pippenger bad events

theorem KaltonRoberts.h_entropy_scale (t a b : ℝ) (ht : t ≠ 0) (ha : a ≠ 0) (hb : b ≠ 0) (hab : a - b ≠ 0) : hEntropy (t * a) (t * b) = t * hEntropy a b

theorem KaltonRoberts.h_entropy_scale_nat (N A B : ℕ) (a b : ℝ) (hN : ↑N ≠ 0) (ha : a ≠ 0) (hb : b ≠ 0) (hab : a - b ≠ 0) (hA : ↑A = ↑N * a) (hB : ↑B = ↑N * b) : hEntropy ↑A ↑B = ↑N * hEntropy a b

theorem KaltonRoberts.choose_ratio_le_entropy_bound (a b k : ℕ) (hk : 0 < k) (hka : k < a) (hkb : k < b) : ↑(a.choose k) / ↑(b.choose k) ≤ (↑b + 1) * Real.exp (hEntropy ↑a ↑k - hEntropy ↑b ↑k)

theorem KaltonRoberts.choose_ratio_le_pow (a b k : ℕ) (hab : a ≤ b) (hk : k ≤ a) : ↑(a.choose k) / ↑(b.choose k) ≤ (↑a / ↑b) ^ k

theorem KaltonRoberts.pippenger_small_term_raw (N L r c m : ℕ) (hm : 0 < m) (hmN : m ≤ N) (hmL : m ≤ L) (hrc : r ≤ c) (hcmN : c * m ≤ r * N) : ↑(N.choose m) * ↑(L.choose m) * ↑((c * m).choose (r * m)) / ↑((r * N).choose (r * m)) ≤ (Real.exp 1 * ↑N / ↑m * (Real.exp 1 * ↑L / ↑m) * (↑(c * m) / ↑(r * N)) ^ r) ^ m

theorem KaltonRoberts.pippenger_term_le_entropy_bound (N L r c m : ℕ) (hm : 0 < m) (hmN : m < N) (hmL : m < L) (hr : 0 < r) (hrc : r < c) : ↑(N.choose m) * ↑(L.choose m) * ↑((c * m).choose (r * m)) / ↑((r * N).choose (r * m)) ≤ (↑(r * N) + 1) * Real.exp (hEntropy ↑N ↑m + hEntropy ↑L ↑m + hEntropy ↑(c * m) ↑(r * m) - hEntropy ↑(r * N) ↑(r * m))

theorem KaltonRoberts.pippenger_entropy_exponent_eq_phi (N L r c m : ℕ) (θ : ℝ) (hN : 0 < N) (hm : 0 < m) (hmN : m < N) (hmL : m < L) (hr : 0 < r) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hLθ : ↑L = θ * ↑N) (hcθ : ↑c = ↑r / θ) : hEntropy ↑N ↑m + hEntropy ↑L ↑m + hEntropy ↑(c * m) ↑(r * m) - hEntropy ↑(r * N) ↑(r * m) = ↑N * Phi (↑r) θ (↑m / ↑N)

theorem KaltonRoberts.pippenger_mid_term_le (N L r c m : ℕ) (θ : ℝ) (hN : 0 < N) (hm : 0 < m) (hmN : m < N) (hmL : m < L) (hr : 0 < r) (hrc : r < c) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hLθ : ↑L = θ * ↑N) (hcθ : ↑c = ↑r / θ) (hphi : Phi (↑r) θ (↑m / ↑N) ≤ -1 / 1000) : ↑(N.choose m) * ↑(L.choose m) * ↑((c * m).choose (r * m)) / ↑((r * N).choose (r * m)) ≤ (↑(r * N) + 1) * Real.exp (-↑N / 1000)

Subset extension

theorem KaltonRoberts.exists_superset_card_eq {α : Type u_1} [Fintype α] (B : Finset α) (m : ℕ) (hBm : B.card ≤ m) (hmA : m ≤ Fintype.card α) : ∃ (T : Finset α), B ⊆ T ∧ T.card = m

Counting constrained permutations with arbitrary subsets

theorem KaltonRoberts.card_subtype_perm_mul_right {n : ℕ} (π : Equiv.Perm (Fin n)) (P : Equiv.Perm (Fin n) → Prop) [DecidablePred P] : Fintype.card { σ : Equiv.Perm (Fin n) // P σ } = Fintype.card { σ : Equiv.Perm (Fin n) // P (σ * π) }

theorem KaltonRoberts.card_subtype_perm_mul_left {n : ℕ} (π : Equiv.Perm (Fin n)) (P : Equiv.Perm (Fin n) → Prop) [DecidablePred P] : Fintype.card { σ : Equiv.Perm (Fin n) // P σ } = Fintype.card { σ : Equiv.Perm (Fin n) // P (π * σ) }

theorem KaltonRoberts.exists_perm_set_to_initial {n : ℕ} (A : Finset (Fin n)) : ∃ (π : Equiv.Perm (Fin n)), ∀ (x : Fin n), x ∈ A ↔ ↑(π x) < A.card

theorem KaltonRoberts.card_constrained_perm_subsets {n : ℕ} (A B : Finset (Fin n)) (hs : A.card ≤ B.card) (ht : B.card ≤ n) : Fintype.card { σ : Equiv.Perm (Fin n) // ∀ a ∈ A, σ a ∈ B } = B.card.descFactorial A.card * (n - A.card).factorial

Good matching existence

theorem KaltonRoberts.right_coverage_of_equiv {N L r c : ℕ} (hc : 0 < c) (σ : Fin N × Fin r ≃ Fin L × Fin c) (w : Fin L) : ∃ (v : Fin N) (e : Fin r), (σ (v, e)).1 = w

theorem KaltonRoberts.first_moment_principle {n : ℕ} (hn : 0 < n.factorial) (weights : Finset (Finset (Fin n) × Finset (Fin n))) (hsum : ∑ p ∈ weights, ↑(Fintype.card { σ : Equiv.Perm (Fin n) // ∀ a ∈ p.1, σ a ∈ p.2 }) / ↑n.factorial < 1) : ∃ (σ : Equiv.Perm (Fin n)), ∀ p ∈ weights, ¬∀ a ∈ p.1, σ a ∈ p.2

theorem KaltonRoberts.good_perm_of_sum_lt (M : ℕ) (_hM : 0 < M) (pairs : Finset (Finset (Fin M) × Finset (Fin M))) (hsum : ∑ p ∈ pairs, ↑(p.2.card.descFactorial p.1.card) * ↑(M - p.1.card).factorial / ↑M.factorial < 1) (hpairs : ∀ p ∈ pairs, p.1.card ≤ p.2.card ∧ p.2.card ≤ M) : ∃ (σ : Equiv.Perm (Fin M)), ∀ p ∈ pairs, ¬∀ a ∈ p.1, σ a ∈ p.2

theorem KaltonRoberts.first_moment_principle_indexed {n : ℕ} {ι : Type u_1} (I : Finset ι) (A B : ι → Finset (Fin n)) (hsum : ∑ i ∈ I, ↑(Fintype.card { σ : Equiv.Perm (Fin n) // ∀ a ∈ A i, σ a ∈ B i }) / ↑n.factorial < 1) : ∃ (σ : Equiv.Perm (Fin n)), ∀ i ∈ I, ¬∀ a ∈ A i, σ a ∈ B i

theorem KaltonRoberts.good_perm_indexed_of_sum_lt {ι : Type u_1} (M : ℕ) (I : Finset ι) (A B : ι → Finset (Fin M)) (hsum : ∑ i ∈ I, ↑((B i).card.descFactorial (A i).card) * ↑(M - (A i).card).factorial / ↑M.factorial < 1) (hpairs : ∀ i ∈ I, (A i).card ≤ (B i).card ∧ (B i).card ≤ M) : ∃ (σ : Equiv.Perm (Fin M)), ∀ i ∈ I, ¬∀ a ∈ A i, σ a ∈ B i

theorem KaltonRoberts.desc_factorial_ratio_eq_choose_ratio (M a k : ℕ) (_hka : k ≤ a) (hkM : k ≤ M) : ↑(a.descFactorial k) * ↑(M - k).factorial / ↑M.factorial = ↑(a.choose k) / ↑(M.choose k)

theorem KaltonRoberts.good_matching_exists_of_ratio_sum_lt_one (N L r c A : ℕ) (_hN : 0 < N) (hL : 0 < L) (hr : 0 < r) (hc : r < c) (hNL : r * N = c * L) (hA : A ≤ L) (hsum : ∑ m ∈ Finset.Icc 1 A, ↑(N.choose m) * ↑(L.choose m) * ↑((c * m).choose (r * m)) / ↑((r * N).choose (r * m)) < 1) : ∃ (edge : Fin N → Fin r → Fin L), (∀ (w : Fin L), ∃ (v : Fin N) (e : Fin r), edge v e = w) ∧ ∀ (S : Finset (Fin N)), S.card ≤ A → (S.biUnion fun (v : Fin N) => Finset.image (edge v) Finset.univ).card ≥ S.card

If the expected number of bad sets is < 1, a good matching exists.

Constructing FiniteExpanderWitness from a good edge function

noncomputable def KaltonRoberts.finiteExpanderOfGoodEdge (N L r A : ℕ) (hN : 0 < N) (edge : Fin N → Fin r → Fin L) (hcov : ∀ (w : Fin L), ∃ (v : Fin N) (e : Fin r), edge v e = w) (hexp : ∀ (S : Finset (Fin N)), S.card ≤ A → (S.biUnion fun (v : Fin N) => Finset.image (edge v) Finset.univ).card ≥ S.card) : FiniteExpanderWitness r

Package a good edge function into a FiniteExpanderWitness.

Equations

• One or more equations did not get rendered due to their size.