Documentation

LeanPool.KaltonRoberts.Numerical

Numerical verification for the Kalton-Roberts bound #

Exact rational-arithmetic verifications for the parameter choices used in the final bound.

Parameter identities and range checks (Section 5) #

source
theorem KaltonRoberts.p₀_eq :
p₀ = 1 - q₀

p₀ = 1 − q₀. Reference: Equation (9) in Section 5 of the companion paper.

source
theorem KaltonRoberts.τ₁_nonneg :
0 ≤ τ₁

0 ≤ τ₁. Reference: paragraph after Equation (10) in Section 5 of the companion paper.

source
theorem KaltonRoberts.τ₁_le_one :
τ₁ ≤ 1

τ₁ ≤ 1. Reference: paragraph after Equation (10) in Section 5 of the companion paper.

source
theorem KaltonRoberts.τ₂_nonneg :
0 ≤ τ₂

0 ≤ τ₂. Reference: paragraph after Equation (10) in Section 5 of the companion paper.

source
theorem KaltonRoberts.τ₂_le_one :
τ₂ ≤ 1

τ₂ ≤ 1. Reference: paragraph after Equation (10) in Section 5 of the companion paper.

source
theorem KaltonRoberts.frequency_identity_case1 :
(1 - τ₁) * q₀ ^ 3 + τ₁ * q₀ ^ 4 = α₁

The frequency identity for Case 1: (1 − τ₁) q₀³ + τ₁ q₀⁴ = α₁. Reference: Equation (10) and the display after it in Section 5 of the companion paper.

source
theorem KaltonRoberts.frequency_identity_case2 :
(1 - τ₂) * p₀ ^ 4 + τ₂ * p₀ ^ 5 = α₂

The frequency identity for Case 2: (1 − τ₂) p₀⁴ + τ₂ p₀⁵ = α₂. Reference: Equation (10) and the display in Case 2 of Section 5 of the companion paper.

source
theorem KaltonRoberts.C₁_lt_C₂ :
C₁ < C₂

C₁ < C₂. Reference: the display after Equation (17) in Section 5 of the companion paper.

source
theorem KaltonRoberts.C₂_lt_KR_upper :
C₂ < krUpper

C₂ < 9919/500. Reference: the display after Equation (17) in Section 5 of the companion paper.

source
theorem KaltonRoberts.C₁_lt_C₂_lt_KR_upper :
C₁ < C₂ ∧ C₂ < krUpper

The combined chain C₁ < C₂ < 9919/500. Reference: the final verification in Section 5 of the companion paper.

Expander parameter checks (Section 4) #

source
def KaltonRoberts.expanderParams :
List (ℚ × ℕ × ℚ)

The four expander triples (α, r, θ) from the table in Section 4 of the companion paper.

Equations
Instances For
    source
    theorem KaltonRoberts.E₁_target_frequency :
    α₁ / (1 / 3) = 3009 / 10000

    Expander E₁ target frequency check: α₁/(1/3) = 3009/10000. This verifies that the target of E₁ feeds into E₂. Reference: display after Equation (13) in Section 5 of the companion paper.

    source
    theorem KaltonRoberts.E₃_target_frequency :
    α₂ / (2 / 7) = 329 / 1250

    Expander E₃ target frequency check: α₂/(2/7) = 329/1250. This verifies that the target of E₃ feeds into E₄. Reference: display after Equation (16) in Section 5 of the companion paper.

    source
    theorem KaltonRoberts.small_set_bound_E₁ :
    739 / 100 * (1 / 3) ^ (1 - 4) * (1 / 100) ^ (4 - 2) < 1 / 20

    The small-set tail bound for δ = 1/100 and E₁: (739/100)(1/3)^{-3}(1/100)^2 < 1/20. Reference: Equation (7) in Section 4 of the companion paper, using e² < 739/100.

    source
    theorem KaltonRoberts.small_set_bound_E₂ :
    739 / 100 * (4 / 7) ^ (1 - 4) * (1 / 100) ^ (4 - 2) < 1 / 20

    Small-set tail bound for E₂. Reference: Equation (7) in Section 4 of the companion paper.

    source
    theorem KaltonRoberts.small_set_bound_E₃ :
    739 / 100 * (2 / 7) ^ (1 - 4) * (1 / 100) ^ (4 - 2) < 1 / 20

    Small-set tail bound for E₃. Reference: Equation (7) in Section 4 of the companion paper.

    source
    theorem KaltonRoberts.small_set_bound_E₄ :
    739 / 100 * (5 / 11) ^ (1 - 5) * (1 / 100) ^ (5 - 2) < 1 / 20

    Small-set tail bound for E₄. Reference: Equation (7) in Section 4 of the companion paper.

    source
    theorem KaltonRoberts.e_sq_lt :
    Real.exp 2 < 739 / 100
    source
    theorem KaltonRoberts.q₀_pow4_le :
    q₀ ^ 4 ≤ 1 / 16

    q₀⁴ ≤ 1/16, which ensures that in Case 2 the pure fourfold intersection has item frequencies at most α₂. Reference: Case 2 of Section 5 of the companion paper: "Its item frequencies are at most q⁴ ≤ 1/16 < α₂".

    source
    theorem KaltonRoberts.one_sixteenth_lt_α₂ :
    1 / 16 < α₂

    1/16 < α₂. Reference: Case 2 of Section 5 of the companion paper.

    Case 1 balancing (Section 5) #

    source
    theorem KaltonRoberts.case1_balance :
    have D₁ := 6 * q₀ + 4 + τ₁ * (2 * q₀ + 2); have A₁ := 10 + 3 / 2 * D₁; (7 / 3 * A₁ + 1 / 2 * 15) / (7 / 3 + 1 / 2) = C₁

    In Case 1, balancing the two recombination inequalities gives M ≤ C₁.

    The two inequalities are: M ≤ A₁ − (1/2) D' where A₁ = 10 + (3/2) D₁ ... (from E₁) M ≤ 15 + (7/3) D' ... (from E₂) and D₁ = 6 q₀ + 4 + τ₁ (2 q₀ + 2). Eliminating D' gives M ≤ (7/3 · A₁ + 1/2 · 15) / (7/3 + 1/2) = C₁.

    Reference: Equations (12)–(14) in Section 5 of the companion paper.

    Case 2 balancing (Section 5) #

    source
    theorem KaltonRoberts.case2_balance :
    have X₀ := 4 * p₀ + 6 + τ₂ * (p₀ + 1); have A₂ := 47 / 5 + 7 / 5 * X₀; (11 / 6 * A₂ + 2 / 5 * (47 / 3)) / (11 / 6 + 2 / 5) = C₂

    In Case 2, balancing the two recombination inequalities gives M ≤ C₂.

    The two inequalities are: M ≤ A₂ − (2/5) Y where A₂ = 47/5 + (7/5) X₀ ... (from E₃) M ≤ 47/3 + (11/6) Y ... (from E₄) and X₀ = 4 p₀ + 6 + τ₂ (p₀ + 1). Eliminating Y gives M ≤ (11/6 · A₂ + 2/5 · 47/3) / (11/6 + 2/5) = C₂.

    Reference: Equations (15)–(17) in Section 5 of the companion paper.

    Convexity check: Φ'' > 3 (Section 4, Equation (8)) #

    source
    theorem KaltonRoberts.Phi''_lower_E₁ (x : ℚ) :
    1 / 100 ≤ x → x ≤ 1003 / 10000 → 3 < (4 - 2) / x + (4 - 1) / (1 - x) - 1 / (1 / 3 - x)
    source
    theorem KaltonRoberts.Phi''_lower_E₂ (x : ℚ) :
    1 / 100 ≤ x → x ≤ 3009 / 10000 → 3 < (4 - 2) / x + (4 - 1) / (1 - x) - 1 / (4 / 7 - x)
    source
    theorem KaltonRoberts.Phi''_lower_E₃ (x : ℚ) :
    1 / 100 ≤ x → x ≤ 47 / 625 → 3 < (4 - 2) / x + (4 - 1) / (1 - x) - 1 / (2 / 7 - x)
    source
    theorem KaltonRoberts.Phi''_lower_E₄ (x : ℚ) :
    1 / 100 ≤ x → x ≤ 329 / 1250 → 3 < (5 - 2) / x + (5 - 1) / (1 - x) - 1 / (5 / 11 - x)