Grothendieck's inequality for bilinear forms on spaces of continuous functions

Let K and L be compact normal spaces (for example compact Hausdorff spaces) and let B be a bilinear form on C(K, 𝕜) × C(L, 𝕜) with ‖B f g‖ ≤ C * ‖f‖ * ‖g‖ for the uniform norms; a continuous bilinear form satisfies this with C = ‖B‖ (ContinuousLinearMap.le_opNorm₂, applied to ContinuousLinearMap.toLinearMap₁₂). For finite families f i in C(K, 𝕜) and g i in C(L, 𝕜) whose square functions ∑ i, ‖f i x‖ ^ 2 and ∑ i, ‖g i y‖ ^ 2 are bounded by one, Grothendieck's inequality bounds ‖∑ i, B (f i) (g i)‖ by the universal constant κ_𝕜 times C, with κ_ℝ = 8 and κ_𝕜 = 16 for a general RCLike field. The constants are those of the matrix inequality and are not optimal.

The proof reduces to Grothendieck's inequality for matrices. Choose finite partitions of unity ρ k on K and σ l on L, indexed by finitely many points, along which the families f and g are uniformly approximated by their values at these points (ContinuousMap.exists_partitionOfUnity_norm_sum_smul_sub_le). The matrix a k l = B (ρ k) (σ l) has scalar bound C, because ∑ k, s k * ρ k has uniform norm at most one whenever every ‖s k‖ ≤ 1 (PartitionOfUnity.norm_sum_smul_le_one), and the approximating sum is ∑ k, ∑ l, a k l * ⟪u k, v l⟫ for the vectors u k = (conj (f i k))ᵢ and v l = (g i l)ᵢ of Euclidean norm at most one. Letting the approximation error tend to zero gives the result.

Main declarations

• LinearMap.norm_sum_apply_apply_le_sixteen_mul: Grothendieck's inequality for bounded bilinear forms on C(K, 𝕜) × C(L, 𝕜) over an RCLike field, with constant 16.
• LinearMap.abs_sum_apply_apply_le_eight_mul: the real version, with constant 8.

References

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

theorem LinearMap.norm_sum_apply_apply_le_sixteen_mul {K : Type u_1} {L : Type u_2} {𝕜 : Type u_3} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [RCLike 𝕜] [Fintype ι] [NormalSpace K] [NormalSpace L] (B : C(K, 𝕜) →ₗ[𝕜] C(L, 𝕜) →ₗ[𝕜] 𝕜) {C : ℝ} (hC : 0 ≤ C) (hB : ∀ (f : C(K, 𝕜)) (g : C(L, 𝕜)), ‖(B f) g‖ ≤ C * ‖f‖ * ‖g‖) {f : ι → C(K, 𝕜)} {g : ι → C(L, 𝕜)} (hf : ∀ (x : K), ∑ i : ι, ‖(f i) x‖ ^ 2 ≤ 1) (hg : ∀ (y : L), ∑ i : ι, ‖(g i) y‖ ^ 2 ≤ 1) : ‖∑ i : ι, (B (f i)) (g i)‖ ≤ 16 * C

Grothendieck's inequality for bounded bilinear forms on spaces of continuous functions, over an RCLike field with constant κ_𝕜 = 16. Let K and L be compact normal spaces and B a bilinear form on C(K, 𝕜) × C(L, 𝕜) with ‖B f g‖ ≤ C * ‖f‖ * ‖g‖, such as a continuous bilinear form with C = ‖B‖. If the families f i in C(K, 𝕜) and g i in C(L, 𝕜) have square functions bounded by one, then ‖∑ i, B (f i) (g i)‖ ≤ 16 * C. Over ℝ, LinearMap.abs_sum_apply_apply_le_eight_mul gives the constant 8.

theorem LinearMap.abs_sum_apply_apply_le_eight_mul {K : Type u_1} {L : Type u_2} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [Fintype ι] [NormalSpace K] [NormalSpace L] (B : C(K, ℝ) →ₗ[ℝ] C(L, ℝ) →ₗ[ℝ] ℝ) {C : ℝ} (hC : 0 ≤ C) (hB : ∀ (f : C(K, ℝ)) (g : C(L, ℝ)), |(B f) g| ≤ C * ‖f‖ * ‖g‖) {f : ι → C(K, ℝ)} {g : ι → C(L, ℝ)} (hf : ∀ (x : K), ∑ i : ι, (f i) x ^ 2 ≤ 1) (hg : ∀ (y : L), ∑ i : ι, (g i) y ^ 2 ≤ 1) : |∑ i : ι, (B (f i)) (g i)| ≤ 8 * C

Grothendieck's inequality for bounded real bilinear forms on spaces of continuous functions, with constant κ_ℝ = 8. Let K and L be compact normal spaces and B a bilinear form on C(K, ℝ) × C(L, ℝ) with |B f g| ≤ C * ‖f‖ * ‖g‖. If ∑ i, f i x ^ 2 ≤ 1 and ∑ i, g i y ^ 2 ≤ 1 everywhere, then |∑ i, B (f i) (g i)| ≤ 8 * C.