The Hilbert-space supremum of a real matrix

For a finite real matrix a : Matrix ι κ ℝ, let Γ(a) be the supremum of |∑ i, ∑ j, a i j * ⟪u i, v j⟫| over all families u : ι → E, v : κ → E of vectors of norm at most one in all real inner product spaces E. Grothendieck's inequality bounds Γ(a) by a universal constant times the supremum of |∑ i, ∑ j, a i j * s i * t j| over scalars |s i|, |t j| ≤ 1, which is the case E = ℝ.

Inner products of finitely many vectors only depend on their span, which has dimension at most card ι + card κ and therefore embeds isometrically into EuclideanSpace ℝ (ι ⊕ κ). We define Matrix.innerProductSup a as the supremum over this single Euclidean space, and prove that it bounds the sum in every real inner product space, in any universe. Together with Matrix.innerProductSup_le_iff, this identifies it with the supremum over all real inner product spaces. It is finite, being at most ∑ i, ∑ j, |a i j|.

The bound in an arbitrary space is what makes Γ(a) usable in the truncation proof of Grothendieck's inequality, where it is applied to Gaussian variables in L² and to their truncation errors, whose norms are small but not at most one; hence the scaled form Matrix.abs_sum_sum_mul_inner_le_innerProductSup_mul_mul.

Main declarations

• Matrix.innerProductSup: the supremum Γ(a).
• Matrix.abs_sum_sum_mul_inner_le_innerProductSup: Γ(a) bounds the sum for unit-ball families in every real inner product space.
• Matrix.abs_sum_sum_mul_inner_le_innerProductSup_mul_mul: the bound Γ(a) * R * S for families of norms at most R and S.
• Matrix.innerProductSup_le_iff: Γ(a) ≤ c as soon as c bounds the sum for unit-ball families in EuclideanSpace ℝ (ι ⊕ κ).
• Matrix.abs_sum_sum_mul_mul_le_innerProductSup: the scalar sum is at most Γ(a).
• Matrix.innerProductSup_le_sum_sum_abs, Matrix.innerProductSup_smul: finiteness and homogeneity.
• Matrix.abs_sum_sum_mul_inner_le_sum_sum_abs: the entrywise bound ∑ i, ∑ j, |a i j| for unit-ball families in any real inner product space.

References

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

noncomputable def Matrix.innerProductSup {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : Matrix ι κ ℝ) : ℝ

The supremum Γ(a) of |∑ i, ∑ j, a i j * ⟪u i, v j⟫| over families of vectors of norm at most one. It is defined in EuclideanSpace ℝ (ι ⊕ κ); by Matrix.abs_sum_sum_mul_inner_le_innerProductSup and Matrix.innerProductSup_le_iff it is the supremum over all real inner product spaces jointly: it bounds the sum in each such space, but the supremum in a single space of small dimension can be strictly smaller.

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

For families of vectors of norm at most one, each inner product has absolute value at most one, so the sum is at most ∑ i, ∑ j, |a i j|.

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

Γ(a) bounds |∑ i, ∑ j, a i j * ⟪u i, v j⟫| for families of vectors of norm at most one in any real inner product space.

theorem Matrix.innerProductSup_le_iff {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {a : Matrix ι κ ℝ} {c : ℝ} : a.innerProductSup ≤ c ↔ ∀ (u : ι → EuclideanSpace ℝ (ι ⊕ κ)) (v : κ → EuclideanSpace ℝ (ι ⊕ κ)), (∀ (i : ι), ‖u i‖ ≤ 1) → (∀ (j : κ), ‖v j‖ ≤ 1) → |∑ i : ι, ∑ j : κ, a i j * inner ℝ (u i) (v j)| ≤ c

Γ(a) is at most c if and only if c bounds |∑ i, ∑ j, a i j * ⟪u i, v j⟫| for families of vectors of norm at most one in EuclideanSpace ℝ (ι ⊕ κ).

theorem Matrix.innerProductSup_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : Matrix ι κ ℝ) : 0 ≤ a.innerProductSup

Γ(a) is nonnegative.

theorem Matrix.innerProductSup_le_sum_sum_abs {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : Matrix ι κ ℝ) : a.innerProductSup ≤ ∑ i : ι, ∑ j : κ, |a i j|

Γ(a) is finite: it is at most the sum of the absolute values of the entries of a.

@[simp]

theorem Matrix.innerProductSup_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] : innerProductSup 0 = 0

The zero matrix has Γ(0) = 0.

theorem Matrix.abs_sum_sum_mul_inner_le_innerProductSup_mul_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : Matrix ι κ ℝ) {u : ι → E} {v : κ → E} {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hu : ∀ (i : ι), ‖u i‖ ≤ R) (hv : ∀ (j : κ), ‖v j‖ ≤ S) : |∑ i : ι, ∑ j : κ, a i j * inner ℝ (u i) (v j)| ≤ a.innerProductSup * R * S

For families of vectors of norms at most R and S in any real inner product space, |∑ i, ∑ j, a i j * ⟪u i, v j⟫| is at most Γ(a) * R * S.

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

The scalar sum |∑ i, ∑ j, a i j * s i * t j| with |s i|, |t j| ≤ 1 is at most Γ(a): this is the case E = ℝ, the trivial direction of Grothendieck's inequality.

theorem Matrix.innerProductSup_smul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (c : ℝ) (a : Matrix ι κ ℝ) : (c • a).innerProductSup = |c| * a.innerProductSup

Γ is absolutely homogeneous.