Sharp inverse norm bound from upper bounds on matrix entries
Let $n \ge 3$, $m > 0$ and $\alpha \ge (n-2)m$, and let $S = \alpha I_n + m\mathbf{1}\mathbf{1}^T$, where $\mathbf{1} \in \mathbb{R}^n$ is the all-ones vector; the range of $\alpha$ makes $S$ diagonally dominant. Write $\|M\|_\infty = \max_i \sum_j |M_{ij}|$. The hypotheses below make $J$ nonsingular. Hillar, Lin and Wibisono proved the companion bound $\|J^{-1}\|_\infty \le \|S^{-1}\|_\infty$ for every symmetric diagonally dominant $J$ with $J_{ij} \ge S_{ij}$ for all $i, j$, with equality only for $J = S$.
Problem. Does every real symmetric $J \in \mathbb{R}^{n \times n}$ with $$0 < J_{ij} \le S_{ij} \quad (1 \le i, j \le n), \qquad J_{ii} \ge \sum_{j \ne i} J_{ij} \quad (1 \le i \le n)$$ satisfy $$\|J^{-1}\|_\infty \ge \|S^{-1}\|_\infty = \frac{\alpha + 2m(n-1)}{\alpha(\alpha + mn)},$$ with equality if and only if $J = S$?
Source: Hillar, Lin and Wibisono (2012), Conjecture 8.1; the range α ≥ (n − 2)m is OpenProblemsInNLA's.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- FA
- Keywords
- diagonally dominant matrices, matrix inverses, OpenProblemsInNLA
References
@misc{hillar2012,
author = {Hillar, Christopher J. and Lin, Shaowei and Wibisono, Andre},
title = {Inverses of symmetric, diagonally dominant positive matrices and applications},
year = {2012},
eprint = {1203.6812},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ie19,
author = {Townsend, Alex},
title = {{IE-19}: Sharp inverse norm bound from upper bounds on matrix entries},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-19/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00083.
namespace RegistryProblems.OP_00083
noncomputable section
open scoped NNReal
/-- The comparison matrix `α I + m 11ᵀ`; the inequalities in IE-19 are entrywise. -/
def comparisonMatrix {n : ℕ} (α m : ℝ) : Matrix (Fin n) (Fin n) ℝ :=
fun i j => (if i = j then α else 0) + m
/-- The exact maximum absolute row-sum norm. The finite supremum is taken in `ℝ≥0`
before coercing to `ℝ`; it is zero for an empty matrix. This is not the default
entrywise supremum norm on a matrix. -/
noncomputable def rowSumNorm {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : ℝ :=
((Finset.univ.sup fun i : Fin n => ∑ j : Fin n, ‖M i j‖₊) : ℝ≥0)
/-- Symmetry, strictly positive entries bounded by the comparison matrix, and
weak diagonal dominance, exactly as in the canonical IE-19 statement. -/
def Admissible {n : ℕ} (α m : ℝ) (J : Matrix (Fin n) (Fin n) ℝ) : Prop :=
J.transpose = J ∧
(∀ i j, 0 < J i j ∧ J i j ≤ comparisonMatrix α m i j) ∧
(∀ i, (∑ j ∈ Finset.univ.erase i, J i j) ≤ J i i)
/-- The displayed proposed lower bound, with all arithmetic over the reals. -/
def comparisonBound (n : ℕ) (α m : ℝ) : ℝ :=
(α + 2 * m * ((n : ℝ) - 1)) / (α * (α + m * (n : ℝ)))
/-- OP-00083: Sharp inverse norm bound from upper bounds on matrix entries -/
def _root_.RegistryProblems.Problem_OP_00083 : Prop :=
∀ n : ℕ, 3 ≤ n → ∀ α m : ℝ, 0 < m → ((n : ℝ) - 2) * m ≤ α →
∀ J : Matrix (Fin n) (Fin n) ℝ, Admissible α m J →
comparisonBound n α m ≤ rowSumNorm J⁻¹ ∧
(rowSumNorm J⁻¹ = comparisonBound n α m ↔ J = comparisonMatrix α m)
end
end RegistryProblems.OP_00083
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_00083 theorem resolution : RegistryProblems.Problem_OP_00083 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00083" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00083 := 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
Proves an admissible real symmetric order-three counterexample using actual matrix inverses and the maximum absolute row-sum norm, then refutes the complete original universal conjecture including its equality clause.
A $3\times3$ positive strictly diagonally dominant matrix refutes the conjectured entrywise inverse-norm inequality $\|J^{-1}\|_\infty\ge\|S^{-1}\|_\infty$ for real symmetric, entrywise positive, diagonally dominant $J$ with $J\le S=\alpha I+m\mathbf 1\mathbf 1^T$ entrywise: for $n=3$ and $m=\alpha=1$, the matrix with diagonal entries $2$ and off-diagonal entries $1/2$ has $\|J^{-1}\|_\infty=7/9<5/4=\|S^{-1}\|_\infty$. Under the stated entrywise upper bounds, the sharp inverse infinity-norm infimum is $1/(\alpha+m)$, rather than …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-19/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00083, "Sharp inverse norm bound from upper bounds on matrix entries", clopen.solutions.