An error bound for homogeneous linear inequalities

Let a j be finitely many linear functionals on a finite-dimensional vector space V over a linearly ordered field, cutting out the polyhedral cone {w | ∀ j, 0 ≤ a j w}. If a vector w violates each of these inequalities by at most c, that is -c ≤ a j w for every j, then w is within O(c) of the cone: there is w' in the cone such that b (w - w') is bounded by C * c for any prescribed finite family of functionals b, with a constant C that depends only on the two families. This is the homogeneous case of Hoffman's error bound. It is stated with the test functionals b instead of a norm, so that it needs no topology on V.

The proof splits the inequalities with Tucker's theorem (TauCeti.exists_nonneg_sum_smul_eq_zero_and_forall_coeff_add_dual_pos). The functionals a j occurring in a nonnegative relation ∑ x j • a j = 0 with x j > 0 vanish on the cone, and on w they are bounded in absolute value by a multiple of c. Projecting w linearly onto their common kernel moves it by O(c). The remaining functionals are strictly positive at a single vector v₀ of that kernel, so adding a multiple O(c) of v₀ lands in the cone.

In toric geometry the bound is applied to the logarithms of absolute values of torus points: a point that nearly satisfies the inequalities cutting out the inverse image of a cone under a linear map is boundedly far from that inverse image. This is what makes analytic toric maps that satisfy the cone-by-cone support condition proper.

Main declarations

• TauCeti.exists_forall_abs_apply_sub_le_of_forall_neg_le: the homogeneous error bound.

References

• A. J. Hoffman, On approximate solutions of systems of linear inequalities, Journal of Research of the National Bureau of Standards 49 (1952), 263–265.
• A. W. Tucker, Dual systems of homogeneous linear relations, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, 1956.

theorem TauCeti.exists_forall_abs_apply_sub_le_of_forall_neg_le {ι : Type u_1} {κ : Type u_2} {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] [LinearOrder K] [IsStrictOrderedRing K] [Finite ι] [Finite κ] [FiniteDimensional K V] (a : ι → Module.Dual K V) (b : κ → Module.Dual K V) : ∃ (C : K), 0 ≤ C ∧ ∀ (c : K), 0 ≤ c → ∀ (w : V), (∀ (j : ι), -c ≤ (a j) w) → ∃ (w' : V), (∀ (j : ι), 0 ≤ (a j) w') ∧ ∀ (k : κ), |(b k) (w - w')| ≤ C * c

Hoffman's error bound for a polyhedral cone. Let a j be finitely many functionals on a finite-dimensional space. There is a constant C such that every w with -c ≤ a j w for all j, where 0 ≤ c, lies within C * c of the cone {w' | ∀ j, 0 ≤ a j w'}, as measured by finitely many prescribed functionals b k. The constant C is nonnegative.