Phi function analysis #

Convexity, endpoint bounds, and interval-negativity proofs for the Phi functions used in the expander table.

Convexity bridge #

theorem KaltonRoberts.convexOn_Icc_neg_of_endpoints {a b : ℝ} {f : ℝ → ℝ} (hab : a ≤ b) (hconv : ConvexOn ℝ (Set.Icc a b) f) (hfa : f a < 0) (hfb : f b < 0) (x : ℝ) (hxa : a ≤ x) (hxb : x ≤ b) :

f x < 0

If f is convex on [a, b] and negative at both endpoints, then f is negative on the entire interval.

Real Phi'' lower bounds #

source

theorem KaltonRoberts.Phi''_lower_real_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_real_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_real_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_real_E₄ (x : ℝ) :

1 / 100 ≤ x → x ≤ 329 / 1250 → 3 < (5 - 2) / x + (5 - 1) / (1 - x) - 1 / (5 / 11 - x)

ConvexOn for Phi on each row interval #

These follow from the generic convexOn_Phi_of_Phi''_nonneg in PhiDeriv.lean, instantiated with the real Phi'' lower bounds proved above.

source

theorem KaltonRoberts.convexOn_Phi_E₁ :

ConvexOn ℝ (Set.Icc (1 / 100) (1003 / 10000)) fun (x : ℝ) => Phi 4 (1 / 3) x

source

theorem KaltonRoberts.convexOn_Phi_E₂ :

ConvexOn ℝ (Set.Icc (1 / 100) (3009 / 10000)) fun (x : ℝ) => Phi 4 (4 / 7) x

source

theorem KaltonRoberts.convexOn_Phi_E₃ :

ConvexOn ℝ (Set.Icc (1 / 100) (47 / 625)) fun (x : ℝ) => Phi 4 (2 / 7) x

source

theorem KaltonRoberts.convexOn_Phi_E₄ :

ConvexOn ℝ (Set.Icc (1 / 100) (329 / 1250)) fun (x : ℝ) => Phi 5 (5 / 11) x

Endpoint Phi upper bounds #

These require atanh-based log certificates from Real.sum_range_sub_log_div_le. Each endpoint bound is a finite computation involving ~8 log evaluations.

source

theorem KaltonRoberts.Phi_E₁_at_delta :

Phi 4 (1 / 3) (1 / 100) < -1 / 1000

source

theorem KaltonRoberts.Phi_E₁_at_alpha :

Phi 4 (1 / 3) (1003 / 10000) < -1 / 1000

source

theorem KaltonRoberts.Phi_E₂_at_delta :

Phi 4 (4 / 7) (1 / 100) < -1 / 1000

source

theorem KaltonRoberts.Phi_E₂_at_alpha :

Phi 4 (4 / 7) (3009 / 10000) < -1 / 1000