Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: foucart-liao-2024-chebyshev-center-regularization bibkey: foucartliao2024sprocedure doi: 10.1007/978-3-031-66497-7_1 url: https://arxiv.org/abs/2310.09677v1 triage: theorem motivation_gids:

  • D5/S3/Analytic/OptimalRecovery/ChebyshevCenterRegularization.result

Foucart–Liao’s Chebyshev-center regularization question

Problem

S. Foucart and C. Liao, S-Procedure Relaxation: a Case of Exactness Involving Chebyshev Centers, arXiv:2310.09677v1, in Explorations in the Mathematics of Data Science (Springer, 2024), DOI 10.1007/978-3-031-66497-7_1, §5 “Some Open Questions”, Question 2:

Is the Chebyshev center always obtained via regularization?

The authors’ gloss is:

From [10], we know that the answer is affirmative under the specific conditions mentioned above, since the Chebyshev center equals the regularizer with parameter satisfying the implicit equation (9). Without the specific conditions, we also know from [8] that the answer is affirmative if one considered the complex setting rather than the real setting.

The section takes and, in (25), and . The “specific conditions” are that is an orthogonal projector and . Equation (8) defines

The Lean claim quantifies over finite-dimensional real Euclidean spaces, linear and , data , and positive bounds . For every nonempty bounded feasible set , it asks whether every Chebyshev center minimizes this objective for some . The counterexample uses , so it also addresses the equal-bound setting of (25).

Motivation

The section describes questions “to which we do not know the answers—we cannot even foretell if any of them are likely to be easily solved”. The positive result under the specific conditions does not settle the unrestricted real case. The declaration D5/S3/Analytic/OptimalRecovery/ChebyshevCenterRegularization.result proves ¬ claim while retaining an orthogonal-projector .

Gap

Preregistration #15463 identifies the tier-1 question. Foucart–Liao, arXiv:2401.11112, concerns the global setting only. Foucart–Hengartner, arXiv:2406.14418, and Lin–Du, arXiv:2506.00704, do not answer this local-center question. These references do not establish exhaustive priority. The source note is Library/Estimation/foucartliao2024sprocedure.md.

ASSUMED-UNVERIFIED: classical work on Chebyshev centers of intersections of two ellipsoids, including Beck–Eldar (2007) and follow-ups, has not been checked for an earlier real instance whose center lies on no regularization path.

Route

Take ,

Here is an orthogonal projector, is invertible, and $\Lambda\Lambda^*=\left(\begin{smallmatrix}1/2&-1/2\-1/2&1\end{smallmatrix}\right) \ne\mathrm{Id}_2f=(x,z)$, feasibility is and , where

The containment certificate is

Feasibility implies , , , and , hence . The feasible contact points

all have squared distance from . Their positive weights sum to one and give, for any ,

Thus every enclosing ball has squared radius at least , and is the unique center with radius . Finally, satisfies

For every the objective at is smaller by . More generally the gap is for with .

Falsifier

The single nonempty bounded real feasible set and its center falsify the universal assertion. Equal positive bounds, an orthogonal projector, and an invertible measurement map are retained. The row-isometry condition fails. Strict domination excludes every ; a failure for only one parameter would not suffice. The comparator improves the objective without changing the model penalty, so no positive residual weight can recover the center.

Evidence

The module’s public definitions are feasible, IsChebyshevCenter, IsRegularizer and claim; its only public theorem is result : ¬ claim. Private projection, measurement, datum and center encode the instance. The private lemmas norm_square and feasible_coordinates give the coordinate reduction; contacts and bounded establish admissibility. The lemma containment proves the polynomial certificate bound, and center_certificate uses the weighted contact identity to compare every enclosing bound. The lemma not_regularizer uses the strict comparator for every . The proof uses exact rational arithmetic and Mathlib. Its accepted axiom closure is ; there is no sorry or additional axiom.

The radius is identified by containment together with attained contact distances. The weighted identity also gives uniqueness; neither radius nor uniqueness is a separate public Lean theorem. The path formula and reflection observation in Triage are not Lean theorems in this module.

Triage

What the settlement shows

  1. Proved (Lean) — real counterexample. The instance above has center and radius , with strict domination by in the squared residual and equality in the squared model norm. No parameter recovers it.

  2. Proved (elementary consequence; not a separate Lean theorem) — mechanism. A minimizer of a positively weighted sum of two penalties is Pareto-optimal for that pair: any point with both penalties no larger and one strictly smaller would lower the sum. A real Chebyshev center can instead be Pareto-dominated in , as this instance shows. Proved in the cited literature (not in this Lean module) — complex distinction. The source’s affirmative complex result relies on exactness of the complex S-procedure; the real counterexample does not contradict that result or the affirmative real result with both specific conditions.

  3. Computed (exact algebra; not in Lean) — regularization path. For the normal equations give the unique minimizer

    Its first coordinate equals only at , where its second coordinate is , rather than .

  4. Proved (paper argument; not in Lean) — projector reflection. Let and , with an orthogonal projector and bounded linear. The subspace is closed since is closed and is finite-dimensional. Write with , . Then , and . Reflection therefore preserves both feasibility norms. For a nonempty bounded feasible set, its unique Hilbert-space Chebyshev center is fixed by this reflection and lies in . Hence Question 1, asking for membership in , can only fail for non-projector in this setting. This observation is separate from the regularization assertion refuted by result.

  5. Open — surviving hypotheses and neighboring questions. Is the center always a regularizer when but is not a projector? Is it always a regularizer when is a projector and for , allowing orthonormal rows up to scaling? The example does not settle either restriction. Question 3, with , and Question 4, concerning near-optimality of the relaxation regularizer, also remain open here. Failure to recover the exact center alone gives no quantitative bound on that regularizer’s near-optimality.

ASSUMED-UNVERIFIED

Classical work on Chebyshev centers of intersections of two ellipsoids, including Beck–Eldar (2007) and follow-ups, has not been checked for an earlier real instance whose center lies on no regularization path. Exhaustive priority is not established. The reflection argument, explicit path formula and general Pareto-optimality observation have no Lean theorem in this module.