Khachiyan's perturbation bounds

Proved

SmaleNinth.khachiyan_perturbation_bounds

by ORdos · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

ellipsoid-methodfarkas-lemmakhachiyanlinear-programming

The ellipsoid method decides a linear system by repeatedly halving the volume of an ellipsoid known to contain the feasible set. For this to terminate, the set must be enclosed in a ball of known radius; for a negative answer to be conclusive, the set must be known to have volume above an explicit floor whenever it is nonempty. A system with integer data satisfies neither condition as given — it may be unbounded, and it may be feasible yet of measure zero. This theorem supplies the standard remedy and its four quantitative guarantees.

Let $U \ge 1$ , let $A \in \mathbb{Z}^{m \times n}$ and $b \in \mathbb{Z}^m$ have all entries bounded by $U$ in absolute value, and let $n \ge 1$ . Write $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$ for the original solution set, and let

\widehat P \;=\; \bigl\{\, x \in \mathbb{R}^n \;\bigm|\; Ax \ge b - \varepsilon\mathbf{1}, \ \ -M \le x_j \le M \ \text{ for all } j \,\bigr\}

be the perturbed-and-boxed solution set, with $\varepsilon = \bigl(2(n+1)(n+1)!\,U^{n+1}\bigr)^{-1}$ and $M = n!\,U^n + 1$ . Then:

Feasibility is preserved in both directions: $P \ne \emptyset$ if and only if $\widehat P \ne \emptyset$ . Relaxing the inequalities by $\varepsilon$ cannot create feasibility, and imposing the box cannot destroy it.
Boundedness: $\widehat P$ is bounded, in the elementary sense that some $K$ bounds every coordinate of every one of its points.
An explicit enclosure: $\widehat P$ is contained in the ball of radius $r = (n+1)M$ centred at the origin.
A volume floor: if $\widehat P$ is nonempty then its Lebesgue measure is at least $v = \bigl(\varepsilon/(nU)\bigr)^{n}$ .

Reading the fourth claim. The bound is non-strict and conditional: nothing is asserted when $\widehat P$ is empty, in which case its measure is of course $0$ . Since $v > 0$ under the standing hypotheses, the claim implies that a nonempty $\widehat P$ is full-dimensional — the property the ellipsoid method actually consumes — but full-dimensionality is a consequence of the stated inequality, not a separate assertion.

Scope. The four claims are exactly the hypotheses that the ellipsoid iteration requires, and they are the only place where integrality of the data is used; the constants are one admissible choice, and any other choice of the same polynomial order supports the same downstream conclusion.

Preamble

import Definitions.Def_Polyhedron
import Definitions.Def_LinearOptimization_Ellipsoid
import Definitions.Def_SmaleNinth_Khachiyan

/-!
The quantitative heart of Khachiyan's theorem: the perturbed-and-boxed
system is feasibility-equivalent to the original integer system, bounded,
contained in an explicit ball, and — when nonempty — of explicitly
bounded-below volume.

Source: L.G. Khachiyan, *A polynomial algorithm in linear programming*,
Soviet Math. Doklady 20 (1979) 191–194; textbook quantification per
B. Korte, J. Vygen, *Combinatorial Optimization*, 6th ed., §4.4–4.5 and
Bertsimas–Tsitsiklis, *Introduction to Linear Optimization*, §8.4 (Lemmas
on full-dimensionality and volume of the perturbed system). The four
claims:

1. `Ax ≥ b` is solvable iff the perturbed-and-boxed system
   `Ax ≥ b − ε𝟙, −M𝟙 ≤ x ≤ M𝟙` is (Farkas with a Cramer-bounded dual
   certificate for one direction, the solution-size bound for the other);
2. the perturbed-and-boxed polyhedron is bounded;
3. it is contained in the ball `E(0, r²I)` with `r = (n+1)M`;
4. when nonempty, its volume is at least `v = (ε/(nU))ⁿ` (it contains a
   cube of side `ε/(nU)` around a solution of sup-norm `≤ M − 1`), so it is
   full-dimensional.

The constants `ε = khachiyanEps n U`, `M = khachiyanBox n U`,
`v = khachiyanVolLB n U`, `r = khachiyanRadius n U` are fixed in
`Definitions.Def_SmaleNinth_Khachiyan`.
-/

open Matrix LinearOptimization

/-- **Khachiyan's perturbation bounds** (Khachiyan 1979; Korte–Vygen
§4.4–4.5; Bertsimas–Tsitsiklis §8.4). For an integer system `Ax ≥ b` in
`n ≥ 1` variables with entries bounded by `U ≥ 1`, the perturbed-and-boxed
system `khachiyanSystemA A · x ≥ khachiyanSystemb n U b` is solvable iff
the original one is; it is bounded and contained in the ball of radius
`khachiyanRadius n U`; and when solvable its solution set has volume at
least `khachiyanVolLB n U` — in particular it is full-dimensional. -/

Formal statement

theorem SmaleNinth.khachiyan_perturbation_bounds {m n : ℕ} (U : ℕ) (hU : 1 ≤ U)
    (hn : 1 ≤ n) (A : Matrix (Fin m) (Fin n) ℤ) (b : Fin m → ℤ)
    (hA : ∀ i j, |A i j| ≤ (U : ℤ)) (hb : ∀ i, |b i| ≤ (U : ℤ)) :
    ((polyhedron (A.map (Int.cast : ℤ → ℝ))
        (fun i => (b i : ℝ))).Nonempty ↔
      (polyhedron (khachiyanSystemA A) (khachiyanSystemb n U b)).Nonempty) ∧
    IsBoundedSet (polyhedron (khachiyanSystemA A) (khachiyanSystemb n U b)) ∧
    polyhedron (khachiyanSystemA A) (khachiyanSystemb n U b) ⊆
      ellipsoidBall 0 (khachiyanRadius n U) ∧
    ((polyhedron (khachiyanSystemA A) (khachiyanSystemb n U b)).Nonempty →
      ENNReal.ofReal (khachiyanVolLB n U) ≤
        MeasureTheory.volume
          (polyhedron (khachiyanSystemA A) (khachiyanSystemb n U b))) := by sorry

Source

L.G. Khachiyan, Soviet Math. Doklady 20 (1979) 191-194; quantification per B. Korte, J. Vygen, Combinatorial Optimization, 6th ed., Sections 4.4-4.5 (esp. the perturbation and volume lemmas), and Bertsimas-Tsitsiklis, Introduction to Linear Optimization, Section 8.4.

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `SmaleNinth.khachiyan_perturbation_bounds`

Setting and hypotheses. The statement fixes natural numbers $m$ and $n$ (implicit; $m = 0$ is allowed), a natural number $U$ with $U \ge 1$ , and assumes $n \ge 1$ . It takes an integer matrix $A \in \mathbb{Z}^{m \times n}$ and an integer vector $b \in \mathbb{Z}^m$ , together with the entrywise bounds $|A_{ij}| \le U$ for all $i, j$ and $|b_i| \le U$ for all $i$ (both comparisons after casting $U$ into $\mathbb{Z}$ ; when $m = 0$ both bound hypotheses are vacuous).

Notation used below. For a real $p \times n$ matrix $C$ and vector $d \in \mathbb{R}^p$ , the polyhedron of the pair $(C, d)$ is the set $\{x \in \mathbb{R}^n \mid d \le Cx\}$ , i.e. $\{x \mid (Cx)_i \ge d_i \text{ for every row } i\}$ ; vectors in $\mathbb{R}^n$ are functions on $\{0, \dots, n-1\}$ . Define the real constants

\varepsilon = \frac{1}{2\,(n+1)\,(n+1)!\,U^{\,n+1}}, \qquad M = n!\,U^{\,n} + 1,

v = \left(\frac{\varepsilon}{n\,U}\right)^{\!n}, \qquad r = (n+1)\,M = (n+1)\,\bigl(n!\,U^{\,n} + 1\bigr).

(Here $v$ is literally the real number $\bigl(\varepsilon / (nU)\bigr)^n$ : the quotient of $\varepsilon$ by the real product $n \cdot U$ , raised to the $n$ -th power. Under the hypotheses $n \ge 1$ , $U \ge 1$ , the denominators are nonzero and $\varepsilon, M, v, r > 0$ .)

The perturbed-and-boxed system is the pair $(\widehat{A}, \widehat{b})$ with $\widehat{A} \in \mathbb{R}^{(m+n+n) \times n}$ and $\widehat{b} \in \mathbb{R}^{m+n+n}$ given rowwise, indexing rows by $i \in \{0, \dots, m+2n-1\}$ :

rows $0 \le i < m$ : $\widehat{A}_{ij} = A_{ij}$ (the integer entry cast to $\mathbb{R}$ ) and $\widehat{b}_i = b_i - \varepsilon$ ;
rows $m \le i < m+n$ : $\widehat{A}_{ij} = 1$ if $j = i - m$ and $0$ otherwise (an $n \times n$ identity block), and $\widehat{b}_i = -M$ ;
rows $m+n \le i < m+2n$ : $\widehat{A}_{ij} = -1$ if $j = i - m - n$ and $0$ otherwise (a negated identity block), and $\widehat{b}_i = -M$ .

So membership of $x \in \mathbb{R}^n$ in the polyhedron $\widehat{P} = \{x \mid \widehat{b} \le \widehat{A}x\}$ says exactly: $(Ax)_i \ge b_i - \varepsilon$ for every $i < m$ , and $x_j \ge -M$ and $-x_j \ge -M$ (i.e. $x_j \le M$ ) for every coordinate $j$ . Write also $P = \{x \in \mathbb{R}^n \mid (Ax)_i \ge b_i \text{ for all } i\}$ for the polyhedron of the original data cast to $\mathbb{R}$ . (When $m = 0$ the system $P$ has no constraints, so $P = \mathbb{R}^n$ and $\widehat{P} = [-M, M]^n$ .)

The conclusion is a conjunction of four claims.

Feasibility equivalence (an iff). $P$ is nonempty if and only if $\widehat{P}$ is nonempty — the left side of the iff is the nonemptiness of the original polyhedron $P$ , the right side the nonemptiness of the perturbed-and-boxed polyhedron $\widehat{P}$ , and both directions are asserted.
Boundedness. $\widehat{P}$ is a bounded set in the following literal sense: there exists a real number $K$ (no positivity required of $K$ ) such that every $x \in \widehat{P}$ satisfies $|x_j| \le K$ for every coordinate $j$ .
Containment in a ball. $\widehat{P} \subseteq E$ , where $E$ is the set $\{x \in \mathbb{R}^n \mid (x - 0)^{\mathsf T}\,(r^2 I)^{-1}\,(x - 0) \le 1\}$ — the "ellipsoid ball" of center $0$ and radius parameter $r$ , defined as the ellipsoid with shape matrix $r^2 I$ ( $I$ the $n \times n$ identity), whose membership condition is the quadratic inequality $x^{\mathsf T}(r^2 I)^{-1}x \le 1$ with the matrix inverse taken in the total (junk-for-singular) sense; since $r > 0$ here, $(r^2 I)^{-1} = r^{-2} I$ and the condition reads $\|x\|_2^2 / r^2 \le 1$ , i.e. $\|x\|_2 \le r$ .
Conditional volume lower bound (an implication with a non-strict inequality). If $\widehat{P}$ is nonempty, then

\operatorname{ofReal}(v) \;\le\; \lambda_n\bigl(\widehat{P}\bigr),

where $\lambda_n$ is Lebesgue measure (volume) on $\mathbb{R}^n$ , valued in $[0, \infty]$ , and $\operatorname{ofReal}(v)$ is the real number $v = (\varepsilon/(nU))^n$ coerced into $[0, \infty]$ (negative reals would be sent to $0$ ; here $v > 0$ ). The inequality is $\le$ , not $<$ ; nothing is asserted about the volume when $\widehat{P}$ is empty. Full-dimensionality (strictly positive volume) is not itself a conjunct — only this $\le$ bound is stated.

The whole statement is asserted for every $m, n, U, A, b$ satisfying the hypotheses above.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by ORdos · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Khachiyan's perturbation bounds

Read-back: SmaleNinth.khachiyan_perturbation_bounds

Read-back: `SmaleNinth.khachiyan_perturbation_bounds`