Grothendieck's theorem: operators from L¹ into Hilbert space are absolutely summing

Let μ be any measure and H an inner product space over 𝕜 = ℝ or ℂ. Every bounded operator T : L¹(μ) → H is absolutely 1-summing, with π₁(T) ≤ κ_𝕜 ‖T‖, where κ_ℝ = 8 and κ_𝕜 = 16 for a general RCLike field are the constants of Grothendieck's inequality for matrices (Matrix.abs_sum_sum_mul_inner_le_eight_mul and Matrix.norm_sum_sum_mul_inner_le_sixteen_mul). The constants are not optimal. The space H need not be complete.

The proof first treats finite families in the span of the indicator functions 1_{A j} of finitely many disjoint sets of finite measure. This span is a weighted finite ℓ¹ space: ‖∑ j, d j • 1_{A j}‖ = ∑ j, μ(A j) * ‖d j‖ (TauCeti.norm_sum_indicatorConstLp_one). For y i = ∑ j, c i j • 1_{A j}, let u i be unit vectors norming T (y i) and v j = T 1_{A j} / (μ(A j) ‖T‖) the normalized columns of T. Then ∑ i, ‖T (y i)‖ = ‖T‖ * ∑ i, ∑ j, c i j * μ(A j) * ⟪u i, v j⟫. The matrix c i j * μ(A j) has scalar bound the weak L¹ norm of y, since a combination of the y i with coefficients of norm at most one has norm at most that weak norm (TauCeti.norm_sum_smul_le_weakLpNorm_one), and Grothendieck's inequality applies. Every finite family of simple functions lies in such a span, the sets A j being the nonzero fibres of the joint simple function. Both sides of the inequality are continuous in the family, so density of simple functions in L¹ gives the general case.

Main results

• ContinuousLinearMap.summingENorm_one_le_ofReal_sixteen_mul_norm: π₁(T) ≤ 16 ‖T‖ for every bounded operator T : L¹(μ, 𝕜) → H over an RCLike field.
• ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm: π₁(T) ≤ 8 ‖T‖ over ℝ.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, Chapter 8.
• J. Diestel, H. Jarchow and A. Tonge, Absolutely Summing Operators, Chapter 3.

theorem ContinuousLinearMap.summingENorm_one_le_ofReal_sixteen_mul_norm {α : Type u_1} {𝕜 : Type u_2} {H : Type u_3} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (T : ↥(MeasureTheory.Lp 𝕜 1 μ) →L[𝕜] H) : summingENorm 1 T ≤ ENNReal.ofReal (16 * ‖T‖)

Grothendieck's theorem. Every bounded operator T from L¹(μ) into an inner product space over an RCLike field is absolutely 1-summing, with π₁(T) ≤ 16 ‖T‖. Over ℝ, ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm gives the constant 8.

theorem ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : ↥(MeasureTheory.Lp ℝ 1 μ) →L[ℝ] H) : summingENorm 1 T ≤ ENNReal.ofReal (8 * ‖T‖)

Grothendieck's theorem over ℝ. Every bounded operator T from real L¹(μ) into a real inner product space is absolutely 1-summing, with π₁(T) ≤ 8 ‖T‖.