Sign averaging and two little-Grothendieck bounds

This file contains an elementary but very useful principle and its two standard consequences for operators with an ℓ_∞ domain or an ℓ₁ codomain.

Sign averaging

For finitely many vectors w j (j ∈ J) in an inner product space, the average of ‖∑_j ε_j w_j‖² over all sign patterns ε ∈ {±1}^J equals ∑_j ‖w_j‖² (the cross terms cancel). Consequently, if every signed sum has norm at most M, then

∑_{j ∈ J} ‖w_j‖² ≤ M².

A sign pattern is encoded by a subset S ⊆ J (ε_j = +1 iff j ∈ S); the corresponding signed sum is signedSum w S J. The averaging identity is sum_powerset_norm_signedSum_sq, proved by induction on J using the parallelogram law, and the resulting inequality is sum_norm_sq_le_sq_of_signedSum_le.

The two consequences

• sum_norm_sq_apply_single_le — for B : ℓ_∞ → H with H a Hilbert space, ∑_j ‖B e_j‖² ≤ ‖B‖². This is the little Grothendieck inequality in the form needed here (with constant 1): only the ±1-vectors of ℓ_∞, which all have norm 1, enter the sign-averaging argument. In Hilbert–Schmidt language: B restricted to the unit vectors is Hilbert–Schmidt with ‖B‖_HS ≤ ‖B‖.
• sum_norm_sq_row_le — dually, for A : H → ℓ₁ with rows w j, i.e. ⟪w j, x⟫ = (A x) j, one has ∑_j ‖w_j‖² ≤ ‖A‖². Here the signed sums are bounded using ∑_{j ∈ J} |y_j| ≤ ‖y‖₁; this is the little Grothendieck bound for the adjoint A' : ℓ_∞ = ℓ₁' → H, but stated without ever forming the adjoint.

Both are stated as bounds on finite partial sums. For the index set ℕ this makes ∑_j ‖w_j‖² summable (summable_norm_sq_row), recorded at the end together with the ℓ₂-norm identity norm_sq_eq_tsum_norm_sq.

Signed sums

def SNumbers.signedSum {G : Type u_1} [AddCommGroup G] {ι : Type u_2} [DecidableEq ι] (w : ι → G) (S J : Finset ι) : G

signedSum w S J = ∑_{j ∈ J} ε_j w_j, where the sign pattern is given by the subset S: ε_j = +1 for j ∈ S and ε_j = -1 for j ∉ S.

Equations

• SNumbers.signedSum w S J = ∑ j ∈ J, if j ∈ S then w j else -w j

@[simp]

theorem SNumbers.signedSum_empty {G : Type u_1} [AddCommGroup G] {ι : Type u_2} [DecidableEq ι] (w : ι → G) (S : Finset ι) : signedSum w S ∅ = 0

The signed sum over the empty index set is 0.

theorem SNumbers.signedSum_insert_of_notMem {G : Type u_1} [AddCommGroup G] {ι : Type u_2} [DecidableEq ι] {w : ι → G} {a : ι} {S J : Finset ι} (ha : a ∉ J) (haS : a ∉ S) : signedSum w S (insert a J) = signedSum w S J - w a

Adding a new index a ∉ J outside the sign pattern subtracts w a.

theorem SNumbers.signedSum_insert_insert {G : Type u_1} [AddCommGroup G] {ι : Type u_2} [DecidableEq ι] {w : ι → G} {a : ι} {S J : Finset ι} (ha : a ∉ J) : signedSum w (insert a S) (insert a J) = signedSum w S J + w a

Adding a new index a ∉ J inside the sign pattern adds w a.

The averaging identity and the sign-averaging bound

theorem SNumbers.sum_powerset_norm_signedSum_sq {ι : Type u_1} [DecidableEq ι] (𝕜 : Type u_2) [RCLike 𝕜] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (w : ι → H) (J : Finset ι) : ∑ S ∈ J.powerset, ‖signedSum w S J‖ ^ 2 = 2 ^ J.card * ∑ j ∈ J, ‖w j‖ ^ 2

Sign averaging (identity form). Summing ‖∑_j ε_j w_j‖² over all 2^|J| sign patterns gives 2^|J| · ∑_{j ∈ J} ‖w_j‖²: the cross terms cancel. The proof is induction on J, where the two extensions of a sign pattern to a new index are paired by the parallelogram law.

The scalar field 𝕜 is an explicit argument because it does not occur in the statement (only the norm does, while the proof uses the inner product).

theorem SNumbers.sum_norm_sq_le_sq_of_signedSum_le {ι : Type u_1} [DecidableEq ι] (𝕜 : Type u_2) [RCLike 𝕜] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {w : ι → H} {J : Finset ι} {M : ℝ} (hM : ∀ S ⊆ J, ‖signedSum w S J‖ ≤ M) : ∑ j ∈ J, ‖w j‖ ^ 2 ≤ M ^ 2

Sign averaging (inequality form). If every signed sum ∑_j ε_j w_j (j ∈ J) has norm at most M, then ∑_{j ∈ J} ‖w_j‖² ≤ M². As above, 𝕜 is explicit since it does not occur in the statement.

Little Grothendieck for an ℓ_∞ domain

theorem SNumbers.signedSum_single_coord {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} [DecidableEq ι] (S J : Finset ι) (i : ι) : ↑(signedSum (fun (j : ι) => lp.single ⊤ j 1) S J) i = if i ∈ J then if i ∈ S then 1 else -1 else 0

The coordinates of a signed sum of unit vectors of ℓ_∞ are 0 and ±1.

theorem SNumbers.norm_signedSum_single_le_one {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} [DecidableEq ι] (S J : Finset ι) : ‖signedSum (fun (j : ι) => lp.single ⊤ j 1) S J‖ ≤ 1

Signed sums of the unit vectors of ℓ_∞ are contained in the unit ball.

theorem SNumbers.sum_norm_sq_apply_single_le {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} [DecidableEq ι] (B : ↥(lp (fun (x : ι) => 𝕜) ⊤) →L[𝕜] H) (J : Finset ι) : ∑ j ∈ J, ‖B (lp.single ⊤ j 1)‖ ^ 2 ≤ ‖B‖ ^ 2

Little Grothendieck inequality for ℓ_∞ → H. For every bounded operator B from ℓ_∞ into a Hilbert space and every finite set J of indices, ∑_{j ∈ J} ‖B e_j‖² ≤ ‖B‖²; that is, B is Hilbert–Schmidt on the unit vectors with ‖B‖_HS ≤ ‖B‖.

The dual bound for an ℓ₁ codomain

theorem SNumbers.sum_norm_apply_le_norm_l1 {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} (f : ↥(lp (fun (x : ι) => 𝕜) 1)) (J : Finset ι) : ∑ j ∈ J, ‖↑f j‖ ≤ ‖f‖

Finite partial sums of the absolute values of the coordinates of an ℓ₁-vector are bounded by its norm.

theorem SNumbers.sum_norm_sq_row_le {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (A : H →L[𝕜] ↥(lp (fun (x : ι) => 𝕜) 1)) {w : ι → H} (hw : ∀ (j : ι) (x : H), inner 𝕜 (w j) x = ↑(A x) j) (J : Finset ι) : ∑ j ∈ J, ‖w j‖ ^ 2 ≤ ‖A‖ ^ 2

Little Grothendieck inequality for H → ℓ₁. If w j are the rows of A : H → ℓ₁, i.e. ⟪w j, x⟫ = (A x) j for all x, then ∑_{j ∈ J} ‖w j‖² ≤ ‖A‖² for every finite J.

This is the little Grothendieck bound applied to the adjoint of A, which maps ℓ_∞ = ℓ₁' into H; formulating it via the rows avoids constructing the adjoint. The signed sums are bounded here by re ⟪z, z⟫ = re (∑_j ε_j (A z)_j) ≤ ‖A z‖₁ ≤ ‖A‖ ‖z‖.

Summability and the ℓ₂-norm as a sum of squares

theorem SNumbers.summable_norm_sq_row {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (A : H →L[𝕜] ↥(lp (fun (x : ℕ) => 𝕜) 1)) {w : ℕ → H} (hw : ∀ (j : ℕ) (x : H), inner 𝕜 (w j) x = ↑(A x) j) : Summable fun (j : ℕ) => ‖w j‖ ^ 2

Over the index set ℕ, the row bound makes ∑_j ‖w_j‖² a convergent series (its partial sums are nonnegative and bounded by ‖A‖²).

theorem SNumbers.norm_sq_eq_tsum_norm_sq {ι : Type u_3} {E : ι → Type u_4} [(i : ι) → NormedAddCommGroup (E i)] (f : ↥(lp E 2)) : ‖f‖ ^ 2 = ∑' (i : ι), ‖↑f i‖ ^ 2

The squared ℓ₂-norm is the sum of the squared coordinate norms.