Grothendieck's inequality for matrices

Let a be a finite scalar matrix with |∑ i, ∑ j, a i j * s i * t j| ≤ C whenever all scalars s i, t j have absolute value at most one. Grothendieck's inequality bounds |∑ i, ∑ j, a i j * ⟪u i, v j⟫| by a universal constant times C, for all families of vectors of norm at most one in any inner product space. We prove it with the constants κ_ℝ = 8 over the reals and κ_𝕜 = 16 over any RCLike field; these constants are not optimal.

The real case

The proof is the Gaussian truncation argument. By Matrix.innerProductSup_le_iff it suffices to treat a finite-dimensional real inner product space E. Its vectors embed isometrically into L² of the standard Gaussian measure on E by TauCeti.Probability.gaussianL2; write uᴹ for the observable of u clipped at height M > 0. Splitting ⟪u, v⟫ = ⟪uᴹ, vᴹ⟫ + ⟪uᴹ, v - vᴹ⟫ + ⟪u - uᴹ, v⟫ in L²:

• the first part is the integral of ∑ i, ∑ j, a i j * uᵢᴹ(y) * vⱼᴹ(y), which is at most C * M ^ 2 pointwise because the clipped observables are bounded by M;
• the clipping errors have L² norm at most √3 / (4 * M), so the other two parts are bounded through Γ(a) = Matrix.innerProductSup a, which applies in every real inner product space.

This gives the absorption inequality Γ(a) ≤ C * M ^ 2 + Γ(a) * √3 / (2 * M) (Matrix.innerProductSup_le_mul_sq_add); at M = 2 it yields Γ(a) ≤ 8 * C.

The RCLike case

Over an RCLike field, rotate the sum by a scalar ω of norm at most one to make it real and nonnegative, and regard the space as a real inner product space via InnerProductSpace.rclikeToReal. The real part of the rotated sum is the sum of two real bilinear expressions, with coefficient matrices re (ω * a i j) and im (ω * a i j), both of which inherit the scalar bound C. Applying the real inequality twice gives 16 * C.

Main declarations

• Matrix.abs_sum_sum_mul_mul_le_mul_sq: the scalar bound rescaled to scalars bounded by M.
• Matrix.innerProductSup_le_mul_sq_add: the absorption inequality.
• Matrix.innerProductSup_le_eight_mul: Γ(a) ≤ 8 * C.
• Matrix.abs_sum_sum_mul_inner_le_eight_mul: the real Grothendieck inequality in any real inner product space.
• Matrix.abs_sum_sum_map_mul_mul_mul_le: real-linear images of a rotated RCLike matrix inherit its scalar bound.
• Matrix.norm_sum_sum_mul_inner_le_sixteen_mul: the Grothendieck inequality over RCLike scalars, in any inner product space.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §8.1.

theorem Matrix.abs_sum_sum_mul_mul_le_mul_sq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : Matrix ι κ ℝ) {C : ℝ} (h : ∀ (s : ι → ℝ) (t : κ → ℝ), (∀ (i : ι), |s i| ≤ 1) → (∀ (j : κ), |t j| ≤ 1) → |∑ i : ι, ∑ j : κ, a i j * s i * t j| ≤ C) {M : ℝ} (hM : 0 < M) {s : ι → ℝ} {t : κ → ℝ} (hs : ∀ (i : ι), |s i| ≤ M) (ht : ∀ (j : κ), |t j| ≤ M) : |∑ i : ι, ∑ j : κ, a i j * s i * t j| ≤ C * M ^ 2

A bound C on |∑ i, ∑ j, a i j * s i * t j| for scalars of absolute value at most one rescales to the bound C * M ^ 2 for scalars of absolute value at most M > 0.

theorem Matrix.innerProductSup_le_mul_sq_add {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : Matrix ι κ ℝ) {C : ℝ} (h : ∀ (s : ι → ℝ) (t : κ → ℝ), (∀ (i : ι), |s i| ≤ 1) → (∀ (j : κ), |t j| ≤ 1) → |∑ i : ι, ∑ j : κ, a i j * s i * t j| ≤ C) {M : ℝ} (hM : 0 < M) : a.innerProductSup ≤ C * M ^ 2 + a.innerProductSup * √3 / (2 * M)

The absorption inequality of the Gaussian truncation proof of Grothendieck's inequality: if |∑ i, ∑ j, a i j * s i * t j| ≤ C for all scalars of absolute value at most one, then Γ(a) ≤ C * M ^ 2 + Γ(a) * √3 / (2 * M) for every clipping height M > 0.

theorem Matrix.innerProductSup_le_eight_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : Matrix ι κ ℝ) {C : ℝ} (h : ∀ (s : ι → ℝ) (t : κ → ℝ), (∀ (i : ι), |s i| ≤ 1) → (∀ (j : κ), |t j| ≤ 1) → |∑ i : ι, ∑ j : κ, a i j * s i * t j| ≤ C) : a.innerProductSup ≤ 8 * C

Grothendieck's inequality in terms of Γ(a) = Matrix.innerProductSup a: if |∑ i, ∑ j, a i j * s i * t j| ≤ C for all real scalars of absolute value at most one, then Γ(a) ≤ 8 * C.

theorem Matrix.abs_sum_sum_mul_inner_le_eight_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : Matrix ι κ ℝ) {C : ℝ} (h : ∀ (s : ι → ℝ) (t : κ → ℝ), (∀ (i : ι), |s i| ≤ 1) → (∀ (j : κ), |t j| ≤ 1) → |∑ i : ι, ∑ j : κ, a i j * s i * t j| ≤ C) {u : ι → E} {v : κ → E} (hu : ∀ (i : ι), ‖u i‖ ≤ 1) (hv : ∀ (j : κ), ‖v j‖ ≤ 1) : |∑ i : ι, ∑ j : κ, a i j * inner ℝ (u i) (v j)| ≤ 8 * C

Grothendieck's inequality over the reals, with constant κ_ℝ = 8: if |∑ i, ∑ j, a i j * s i * t j| ≤ C for all real scalars of absolute value at most one, then |∑ i, ∑ j, a i j * ⟪u i, v j⟫| ≤ 8 * C for all families of vectors of norm at most one in any real inner product space.

theorem Matrix.abs_sum_sum_map_mul_mul_mul_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {𝕜 : Type u_3} [RCLike 𝕜] (a : Matrix ι κ 𝕜) {C : ℝ} (h : ∀ (s : ι → 𝕜) (t : κ → 𝕜), (∀ (i : ι), ‖s i‖ ≤ 1) → (∀ (j : κ), ‖t j‖ ≤ 1) → ‖∑ i : ι, ∑ j : κ, a i j * s i * t j‖ ≤ C) {ω : 𝕜} (hω : ‖ω‖ ≤ 1) (φ : 𝕜 →L[ℝ] ℝ) (hφ : ∀ (z : 𝕜), |φ z| ≤ ‖z‖) {s : ι → ℝ} {t : κ → ℝ} (hs : ∀ (i : ι), |s i| ≤ 1) (ht : ∀ (j : κ), |t j| ≤ 1) : |∑ i : ι, ∑ j : κ, φ (ω * a i j) * s i * t j| ≤ C

If ‖∑ i, ∑ j, a i j * s i * t j‖ ≤ C for all scalars of norm at most one, then for every ω of norm at most one and every real-linear functional φ with |φ z| ≤ ‖z‖ (such as re or im), the real matrix φ (ω * a i j) satisfies the same bound C on real scalars of absolute value at most one.

theorem Matrix.norm_sum_sum_mul_inner_le_sixteen_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (a : Matrix ι κ 𝕜) {C : ℝ} (h : ∀ (s : ι → 𝕜) (t : κ → 𝕜), (∀ (i : ι), ‖s i‖ ≤ 1) → (∀ (j : κ), ‖t j‖ ≤ 1) → ‖∑ i : ι, ∑ j : κ, a i j * s i * t j‖ ≤ C) {u : ι → E} {v : κ → E} (hu : ∀ (i : ι), ‖u i‖ ≤ 1) (hv : ∀ (j : κ), ‖v j‖ ≤ 1) : ‖∑ i : ι, ∑ j : κ, a i j * inner 𝕜 (u i) (v j)‖ ≤ 16 * C

Grothendieck's inequality over an RCLike field, with constant κ_𝕜 = 16: if ‖∑ i, ∑ j, a i j * s i * t j‖ ≤ C for all scalars of norm at most one, then ‖∑ i, ∑ j, a i j * ⟪u i, v j⟫‖ ≤ 16 * C for all families of vectors of norm at most one in any inner product space over 𝕜. Over ℝ, Matrix.abs_sum_sum_mul_inner_le_eight_mul gives the constant 8.