Uniqueness of the right inverse minimizing an induced p-to-2 norm
Let $1 \le m < n$, let $A \in \mathbb{C}^{m \times n}$ have rank $m$, and let $2 < p < \infty$. For $X \in \mathbb{C}^{n \times m}$ let $$\|X\|_{p \to 2} = \sup_{y \in \mathbb{C}^m \setminus \{0\}} \frac{\|Xy\|_2}{\|y\|_p}$$ be the norm induced by the $\ell^p$ norm on $\mathbb{C}^m$ and the Euclidean norm on $\mathbb{C}^n$. Dokmanić and Gribonval showed that the Moore–Penrose inverse $A^\dagger = A^*(AA^*)^{-1}$ minimises this norm among the right inverses of $A$, the $X$ with $AX = I_m$, for every $1 \le p \le \infty$, and that for $p \le 2$ it need not be the only minimiser.
Problem. Is $A^\dagger$ always the unique minimiser? Equivalently, does every $X \in \mathbb{C}^{n \times m}$ with $AX = I_m$ and $X \ne A^\dagger$ satisfy $\|X\|_{p \to 2} > \|A^\dagger\|_{p \to 2}$, for all such $m$, $n$, $A$ and $p$?
Source: Dokmanić and Gribonval (2017), Remark 4.1, the question for ‖X‖_{p→2}; they ask it also for ‖XA‖_{p→2}.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- FA
- Keywords
- generalized inverses, induced norms, OpenProblemsInNLA
References
@misc{dokmanic2017,
author = {Dokmani{\'c}, Ivan and Gribonval, R{\'e}mi},
title = {Beyond {M}oore--{P}enrose {P}art {I}: Generalized inverses that minimize matrix norms},
year = {2017},
eprint = {1706.08349},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ie23,
author = {Townsend, Alex},
title = {{IE-23}: Uniqueness of the right inverse minimizing an induced p-to-2 norm},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-23/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00084.
namespace RegistryProblems.OP_00084
noncomputable section
open scoped BigOperators Classical
abbrev Vec (n : ℕ) := Fin n → ℂ
abbrev Mat (m n : ℕ) := Matrix (Fin m) (Fin n) ℂ
/-- The genuine complex Euclidean norm, rather than the default supremum
norm on a function space. -/
def euclideanNorm {n : ℕ} (y : Vec n) : ℝ :=
‖(WithLp.toLp 2 y : EuclideanSpace ℂ (Fin n))‖
/-- The original finite-real-p denominator, defined by the displayed sum and
real power. The canonical conjecture uses only 2 < p, so neither p=2 nor an
infinite-p endpoint is silently included. Positivity for nonzero vectors is a
theorem obligation, not a premise added to the conjecture. -/
def lpNorm {n : ℕ} (p : ℝ) (y : Vec n) : ℝ :=
(∑ i, ‖y i‖ ^ p) ^ (1 / p)
/-- Every actual ratio from a nonzero right-hand side. Matrix multiplication
acts on the input vector before taking its Euclidean norm. -/
def ratioSet {m n : ℕ} (p : ℝ) (X : Mat n m) : Set ℝ :=
{r | ∃ y : Vec m, y ≠ 0 ∧ r = euclideanNorm (X.mulVec y) / lpNorm p y}
/-- The genuine supremum in the canonical definition. Generic nonemptiness,
boundedness, and the least-upper-bound property must all be proved on the
original domain; no default value of a conditional supremum is used as a
counterexample. -/
def inducedNorm {m n : ℕ} (p : ℝ) (X : Mat n m) : ℝ := sSup (ratioSet p X)
/-- Actual matrix rank, equal to the dimension of the complex linear range. -/
def FullRowRank {m n : ℕ} (A : Mat m n) : Prop := A.rank = m
/-- The Moore-Penrose formula used in the canonical full-row-rank statement,
with Mathlib's genuine totalized matrix inverse. Invertibility and the exact
inverse value for the witness must be established; no proposed inverse is
substituted into this definition. -/
def moorePenrose {m n : ℕ} (A : Mat m n) : Mat n m :=
A.conjTranspose * (A * A.conjTranspose)⁻¹
def IsRightInverse {m n : ℕ} (A : Mat m n) (X : Mat n m) : Prop := A * X = 1
/-- OP-00084: Uniqueness of the right inverse minimizing an induced p-to-2 norm -/
def _root_.RegistryProblems.Problem_OP_00084 : Prop :=
∀ m n : ℕ, 1 ≤ m → m < n → ∀ A : Mat m n, FullRowRank A →
∀ p : ℝ, 2 < p → ∀ X : Mat n m,
IsRightInverse A X → X ≠ moorePenrose A →
inducedNorm p (moorePenrose A) < inducedNorm p X
end
end RegistryProblems.OP_00084
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00084 theorem resolution : RegistryProblems.Problem_OP_00084 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00084" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00084 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Complete negative answer to the original direct induced p-to-2 norm uniqueness conjecture, with two distinct global minimizers at the exact admissible p=4 witness.
Every right inverse of a full-row-rank $A\in\mathbb C^{m\times n}$ has the form $A^\dagger+N$ with $AN=0$, and $\|(A^\dagger+N)z\|_2^2=\|A^\dagger z\|_2^2+\|Nz\|_2^2$, so the Moore–Penrose inverse minimizes the induced $\ell^p\to\ell^2$ norm among right inverses for every $p$. A single $2\times3$ full-row-rank matrix nevertheless has, for every $2<p<\infty$ and over both fields, multiple right inverses minimizing this norm, with common norm $2^{1/2-1/p}$. The complete minimizer …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-23/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00084, "Uniqueness of the right inverse minimizing an induced p-to-2 norm", clopen.solutions.