Deterministic sampling-deviation bound $|D_{\Omega,t}(AC^\top,BD^\top)|\le\|\Omega-tJ\|\cdot(\text{row factors})$ (Chen–Li Lemma 4.4)

Read-back — theorem MatrixCompletion.NoSpuriousMin.sampling_deviation_bound

For every triple of natural numbers $d, r_1, r_2$ (each possibly $0$), every finite set $\Omega$ of index pairs $(i,j)$ with $i, j \in \{1,\dots,d\}$, every real number $t$ (arbitrary: possibly negative, zero, or greater than $1$), and every quadruple of real matrices $A \in \mathbb{R}^{d\times r_1}$, $B \in \mathbb{R}^{d\times r_2}$, $C \in \mathbb{R}^{d\times r_1}$, $D \in \mathbb{R}^{d\times r_2}$ — with no hypothesis whatsoever on $\Omega$, $t$, or the matrices (in particular $\Omega$ need not be symmetric, and $t$ need not lie in $[0,1]$) — the following inequality is asserted:

where the notation unfolds as follows.

• For $d\times d$ real matrices $M, N$, the quantity $\mathrm{dev}_{\Omega,t}(M,N)$ (the file's sampDev) is defined as

where $\langle X, Y\rangle = \sum_{i,j} X_{ij}Y_{ij}$ is the entrywise (Frobenius) inner product, and $P_\Omega M$ is the matrix that agrees with $M$ on entries $(i,j) \in \Omega$ and is $0$ elsewhere. Thus $\langle P_\Omega M, P_\Omega N\rangle = \sum_{(i,j)\in\Omega} M_{ij}N_{ij}$.

• The left-hand argument is $M = AC^{\mathsf T}$, i.e. $M_{ij} = \sum_{k=1}^{r_1} A_{ik}C_{jk} = \langle A_i, C_j\rangle$ (inner product of row $i$ of $A$ with row $j$ of $C$); likewise $N = BD^{\mathsf T}$ with $N_{ij} = \langle B_i, D_j\rangle$. Note the pairing: $A$ with $C$ forms the first argument and $B$ with $D$ the second, while on the right-hand side the sums pair $A$ with $B$ and $C$ with $D$.

• $\sigma_{\Omega,t}$ (the file's sampDevNorm) is defined as $\sigma_{\max}(S_\Omega - t\,\mathbf 1\mathbf 1^{\mathsf T})$, where $S_\Omega$ is the $d\times d$ $\{0,1\}$-matrix with $(S_\Omega)_{ij}=1$ exactly when $(i,j)\in\Omega$, and $t\,\mathbf 1\mathbf 1^{\mathsf T}$ is $t$ times the all-ones matrix. Here $\sigma_{\max}(X)$ is not Mathlib's operator norm but a custom definition: the supremum, over vectors $v \in \mathbb{R}^d$ satisfying $\sqrt{\sum_j v_j^2} = 1$, of $\sqrt{\sum_i (Xv)_i^2}$. This supremum is taken in the real numbers, so by convention it equals $0$ when the index set is empty — in particular, when $d = 0$ there are no unit vectors and $\sigma_{\Omega,t} = 0$ (in that degenerate case both sides of the inequality are $0$ and the claim holds trivially).

• $\lVert v \rVert$ denotes the Euclidean norm $\sqrt{\sum_j v_j^2}$ of a vector (the file's vecNorm), and $A_k$ denotes the $k$-th row of $A$; the two square-root factors are therefore $\sqrt{\sum_{k} \lVert A_k\rVert^2 \lVert B_k\rVert^2}$ and $\sqrt{\sum_{k} \lVert C_k\rVert^2 \lVert D_k\rVert^2}$, each sum running over the $d$ rows. These are not products of full Frobenius norms: each is a single square root of a row-wise coupled sum (by Cauchy–Schwarz such a factor is at most $\|A\|_{2,\infty}\|B\|_F$, etc., but the statement asserts the coupled form, not any such relaxation).

Degenerate cases silently included: $d = 0$ or $\Omega = \varnothing$ (then $\mathrm{dev}$ reduces to $-t\langle M,N\rangle$ while $\sigma_{\Omega,t} = \sigma_{\max}(-t\mathbf 1\mathbf 1^{\mathsf T})$); $r_1 = 0$ or $r_2 = 0$ (then $AC^{\mathsf T}$ or $BD^{\mathsf T}$ is the zero matrix and the corresponding row norms are $0$, making the left side $0$); and, since $\sigma_{\max}$ is a bare real supremum, any situation in which that supremum were not attained or the set unbounded would yield the Lean convention value rather than an extended-real supremum.