Absolutely summing operators

Let 1 ≤ p ≤ ∞. A bounded operator T : E →L[𝕜] F is absolutely p-summing if there is a constant C such that the Lᵖ norm of (T xᵢ)ᵢ, which is (∑ ‖T xᵢ‖ᵖ)^(1/p) for finite p, is at most C * weakLpNorm p x for every finite family x in E; the least such constant is the p-summing norm πₚ(T). We record πₚ(T) as the extended gauge ContinuousLinearMap.summingENorm p T ∈ [0, ∞], the supremum over finite families of the ratio of the two sides. It is finite exactly on the absolutely p-summing operators, which form the submodule TauCeti.absolutelySummingOperators 𝕜 p E F of E →L[𝕜] F.

The gauge is absolutely homogeneous and subadditive, satisfies the two-sided ideal inequality πₚ(A ∘ T ∘ B) ≤ ‖A‖ πₚ(T) ‖B‖, dominates the operator norm, takes the value ‖f‖ ‖y‖ on the rank-one operator x ↦ f x • y, and is lower semicontinuous for the operator-norm topology, which is the input for completeness of the summing-norm ideal; all of this holds over any nontrivially normed field. Over real or complex scalars, at exponent ∞ it is the operator norm, and it decreases as the exponent grows: π_q(T) ≤ π_p(T) for p ≤ q, so absolutely p-summing operators are absolutely q-summing.

Over real or complex scalars, at exponent 1, an operator is absolutely summing exactly when it sends unconditionally convergent series to absolutely convergent series, with no completeness assumption. One direction bounds the weak L¹ norms of the partial families of a summable family; the other concatenates finite families of small weak norm whose images have L¹ norm one.

Packaged as an operator gauge, πₚ gives the normed operator ideal TauCeti.AbsolutelySumming 𝕜 p E F, written Πₚ(E, F). Its norm is πₚ, it is a Banach space whenever F is complete, and it contains the rank-one operators with norm ‖f‖ ‖y‖. Composition with bounded operators on either side and, over real or complex scalars, the inclusion Πₚ(E, F) → Π_q(E, F) for p ≤ q are bounded linear maps between these ideals, of norm at most ‖A‖, ‖B‖ and 1.

Main declarations

• ContinuousLinearMap.summingENorm: the extended p-summing gauge πₚ(T).
• ContinuousLinearMap.summingENorm_le_ofReal_iff: πₚ(T) ≤ C iff the defining inequality holds with constant C.
• ContinuousLinearMap.enorm_toLp_le_summingENorm_mul: the defining inequality with the constant πₚ(T), for families indexed by any finite type.
• ContinuousLinearMap.summingENorm_comp_comp_le: the ideal inequality.
• ContinuousLinearMap.enorm_le_summingENorm: ‖T‖ ≤ πₚ(T).
• ContinuousLinearMap.summingENorm_smulRight: the rank-one value.
• ContinuousLinearMap.lowerSemicontinuous_summingENorm: lower semicontinuity.
• ContinuousLinearMap.summingENorm_top: π_∞(T) = ‖T‖.
• ContinuousLinearMap.summingENorm_le_summingENorm_of_exponent_le: π_q(T) ≤ π_p(T) for p ≤ q.
• TauCeti.absolutelySummingOperators: the submodule of absolutely p-summing operators.
• TauCeti.absolutelySummingOperators_le_of_exponent_le: the inclusion of these submodules.
• TauCeti.mem_absolutelySummingOperators_one_iff: absolutely 1-summing operators are those sending unconditionally summable series to absolutely summable series.
• TauCeti.summingGauge: the p-summing gauge as an operator gauge.
• TauCeti.AbsolutelySumming: the normed operator ideal Πₚ(E, F), complete when F is.
• TauCeti.AbsolutelySumming.norm_smulRight: the rank-one norm in Πₚ(E, F).
• TauCeti.AbsolutelySumming.postcomp, TauCeti.AbsolutelySumming.precomp: composition with bounded operators, with the ideal inequalities norm_postcomp_le and norm_precomp_le.
• TauCeti.AbsolutelySumming.inclusion: the contraction Πₚ(E, F) → Π_q(E, F) for p ≤ q.

References

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

noncomputable def ContinuousLinearMap.summingENorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] (T : E →L[𝕜] F) : ENNReal

The extended absolutely p-summing gauge πₚ(T) ∈ [0, ∞]: the supremum over finite families x of the Lᵖ norm of (T xᵢ)ᵢ divided by the weak Lᵖ norm of x. A family of zero weak norm whose image is not null contributes ∞. It is the least constant in the defining inequality of absolutely p-summing operators (summingENorm_le_ofReal_iff).

theorem ContinuousLinearMap.summingENorm_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] (T : E →L[𝕜] F) : summingENorm p T = ⨆ (n : ℕ), ⨆ (x : Fin n → E), ‖WithLp.toLp p fun (i : Fin n) => T (x i)‖ₑ / ENNReal.ofReal ((TauCeti.weakLpNorm p) x)

The p-summing gauge as a supremum of ratios over families indexed by Fin n.

theorem ContinuousLinearMap.enorm_toLp_div_le_summingENorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (T : E →L[𝕜] F) {n : ℕ} (x : Fin n → E) : ‖WithLp.toLp p fun (i : Fin n) => T (x i)‖ₑ / ENNReal.ofReal ((TauCeti.weakLpNorm p) x) ≤ summingENorm p T

Each finite family bounds the gauge from below by the ratio of its two norms.

theorem ContinuousLinearMap.summingENorm_le_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {T : E →L[𝕜] F} {C : ENNReal} (hC : C ≠ ⊤) : summingENorm p T ≤ C ↔ ∀ (n : ℕ) (x : Fin n → E), ‖WithLp.toLp p fun (i : Fin n) => T (x i)‖ₑ ≤ C * ENNReal.ofReal ((TauCeti.weakLpNorm p) x)

A finite upper bound on the gauge is a bound in the defining inequality, in extended form.

theorem ContinuousLinearMap.summingENorm_le_ofReal_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {T : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) : summingENorm p T ≤ ENNReal.ofReal C ↔ ∀ (n : ℕ) (x : Fin n → E), ‖WithLp.toLp p fun (i : Fin n) => T (x i)‖ ≤ C * (TauCeti.weakLpNorm p) x

The gauge is at most C exactly when the Lᵖ norm of (T xᵢ)ᵢ is at most C * weakLpNorm p x for every finite family x.

theorem ContinuousLinearMap.enorm_toLp_le_summingENorm_mul_of_ne_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {T : E →L[𝕜] F} (hT : summingENorm p T ≠ ⊤) {ι : Type u_6} [Fintype ι] (x : ι → E) : ‖WithLp.toLp p fun (i : ι) => T (x i)‖ₑ ≤ summingENorm p T * ENNReal.ofReal ((TauCeti.weakLpNorm p) x)

A finite gauge bounds the image of every finite family, whatever its index type.

theorem ContinuousLinearMap.norm_toLp_le_toReal_summingENorm_mul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {T : E →L[𝕜] F} (hT : summingENorm p T ≠ ⊤) {ι : Type u_6} [Fintype ι] (x : ι → E) : ‖WithLp.toLp p fun (i : ι) => T (x i)‖ ≤ (summingENorm p T).toReal * (TauCeti.weakLpNorm p) x

The real form of the defining inequality with constant πₚ(T), for an operator of finite gauge.

theorem ContinuousLinearMap.summingENorm_eq_zero_of_norm_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {T : E →L[𝕜] F} (hT : ‖T‖ = 0) : summingENorm p T = 0

An operator of zero operator norm has zero gauge.

@[simp]

theorem ContinuousLinearMap.summingENorm_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] : summingENorm p 0 = 0

The zero operator has zero gauge.

@[simp]

theorem ContinuousLinearMap.summingENorm_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (c : 𝕜) (T : E →L[𝕜] F) : summingENorm p (c • T) = ‖c‖ₑ * summingENorm p T

Absolute homogeneity of the gauge, including its infinite values.

@[simp]

theorem ContinuousLinearMap.summingENorm_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (T : E →L[𝕜] F) : summingENorm p (-T) = summingENorm p T

Negation preserves the gauge.

theorem ContinuousLinearMap.summingENorm_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (S T : E →L[𝕜] F) : summingENorm p (S + T) ≤ summingENorm p S + summingENorm p T

The gauge is subadditive.

theorem ContinuousLinearMap.summingENorm_comp_left_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] (A : F →L[𝕜] G) (T : E →L[𝕜] F) : summingENorm p (A ∘SL T) ≤ ‖A‖ₑ * summingENorm p T

Composing on the left with a bounded operator multiplies the gauge by at most its norm.

theorem ContinuousLinearMap.summingENorm_comp_right_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] (T : F →L[𝕜] G) (B : E →L[𝕜] F) : summingENorm p (T ∘SL B) ≤ summingENorm p T * ‖B‖ₑ

Composing on the right with a bounded operator multiplies the gauge by at most its norm.

theorem ContinuousLinearMap.summingENorm_comp_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] {p : ENNReal} [Fact (1 ≤ p)] (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) : summingENorm p (A ∘SL T ∘SL B) ≤ ‖A‖ₑ * summingENorm p T * ‖B‖ₑ

The two-sided ideal inequality πₚ(A ∘ T ∘ B) ≤ ‖A‖ πₚ(T) ‖B‖.

theorem ContinuousLinearMap.summingENorm_smulRight_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (f : StrongDual 𝕜 E) (y : F) : summingENorm p (smulRight f y) ≤ ‖f‖ₑ * ‖y‖ₑ

The rank-one operator x ↦ f x • y has gauge at most ‖f‖ ‖y‖.

theorem ContinuousLinearMap.enorm_le_summingENorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (T : E →L[𝕜] F) : ‖T‖ₑ ≤ summingENorm p T

The p-summing gauge dominates the operator norm.

@[simp]

theorem ContinuousLinearMap.summingENorm_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : summingENorm p T = 0 ↔ T = 0

The gauge vanishes exactly at zero for maps into a separated normed space.

@[simp]

theorem ContinuousLinearMap.summingENorm_smulRight {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (f : StrongDual 𝕜 E) (y : F) : summingENorm p (smulRight f y) = ‖f‖ₑ * ‖y‖ₑ

The rank-one operator x ↦ f x • y has gauge ‖f‖ ‖y‖.

theorem ContinuousLinearMap.lowerSemicontinuous_summingENorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] : LowerSemicontinuous (summingENorm p)

The p-summing gauge is lower semicontinuous for the operator-norm topology.

theorem ContinuousLinearMap.norm_toLp_eq_zero_of_weakLpNorm_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (T : E →L[𝕜] F) {ι : Type u_4} [Fintype ι] {x : ι → E} (hx : (TauCeti.weakLpNorm p) x = 0) : ‖WithLp.toLp p fun (i : ι) => T (x i)‖ = 0

A bounded operator maps a family of zero weak norm to a family of zero Lᵖ norm.

theorem ContinuousLinearMap.enorm_toLp_le_summingENorm_mul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] (T : E →L[𝕜] F) {ι : Type u_4} [Fintype ι] (x : ι → E) : ‖WithLp.toLp p fun (i : ι) => T (x i)‖ₑ ≤ summingENorm p T * ENNReal.ofReal ((TauCeti.weakLpNorm p) x)

The defining inequality with the constant πₚ(T), for families indexed by any finite type. Over real or complex scalars no finiteness assumption is needed.

@[simp]

theorem ContinuousLinearMap.summingENorm_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : summingENorm ⊤ T = ‖T‖ₑ

At exponent ∞ the summing gauge is the operator norm.

theorem ContinuousLinearMap.summingENorm_le_summingENorm_of_exponent_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {q : ENNReal} [Fact (1 ≤ q)] (hpq : p ≤ q) (T : E →L[𝕜] F) : summingENorm q T ≤ summingENorm p T

Inclusion of summing operators. The summing gauge decreases as the exponent grows: π_q(T) ≤ π_p(T) for p ≤ q.

def TauCeti.absolutelySummingOperators (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (p : ENNReal) [Fact (1 ≤ p)] (E : Type u_2) (F : Type u_3) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Submodule 𝕜 (E →L[𝕜] F)

The absolutely p-summing operators from E to F: the bounded operators of finite p-summing gauge.

@[simp]

theorem TauCeti.mem_absolutelySummingOperators {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T ∈ absolutelySummingOperators 𝕜 p E F ↔ ContinuousLinearMap.summingENorm p T < ⊤

Membership in the submodule means finite gauge.

theorem TauCeti.mem_absolutelySummingOperators_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T ∈ absolutelySummingOperators 𝕜 p E F ↔ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (x : Fin n → E), ‖WithLp.toLp p fun (i : Fin n) => T (x i)‖ ≤ C * (weakLpNorm p) x

An operator is absolutely p-summing iff for some constant C the Lᵖ norm of (T xᵢ)ᵢ is at most C * weakLpNorm p x for every finite family x.

theorem TauCeti.comp_left_mem_absolutelySummingOperators {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (A : F →L[𝕜] G) {T : E →L[𝕜] F} (hT : T ∈ absolutelySummingOperators 𝕜 p E F) : A ∘SL T ∈ absolutelySummingOperators 𝕜 p E G

Absolutely summing operators are stable under composition on the left.

theorem TauCeti.comp_right_mem_absolutelySummingOperators {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {T : F →L[𝕜] G} (hT : T ∈ absolutelySummingOperators 𝕜 p F G) (B : E →L[𝕜] F) : T ∘SL B ∈ absolutelySummingOperators 𝕜 p E G

Absolutely summing operators are stable under composition on the right.

theorem TauCeti.smulRight_mem_absolutelySummingOperators {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : StrongDual 𝕜 E) (y : F) : ContinuousLinearMap.smulRight f y ∈ absolutelySummingOperators 𝕜 p E F

Rank-one operators are absolutely summing.

theorem TauCeti.absolutelySummingOperators_le_of_exponent_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] (hpq : p ≤ q) : absolutelySummingOperators 𝕜 p E F ≤ absolutelySummingOperators 𝕜 q E F

Absolutely p-summing operators are absolutely q-summing for p ≤ q.

Absolutely 1-summing operators and unconditional summability

theorem TauCeti.summable_norm_apply_of_mem_absolutelySummingOperators_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T ∈ absolutelySummingOperators 𝕜 1 E F) {ι : Type u_4} {x : ι → E} (hx : Summable x) : Summable fun (i : ι) => ‖T (x i)‖

An absolutely 1-summing operator sends unconditionally summable families to absolutely summable families.

theorem TauCeti.mem_absolutelySummingOperators_one_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T ∈ absolutelySummingOperators 𝕜 1 E F ↔ ∀ (x : ℕ → E), Summable x → Summable fun (n : ℕ) => ‖T (x n)‖

Absolutely 1-summing operators and series. An operator is absolutely 1-summing exactly when it sends unconditionally convergent series to absolutely convergent series. This is usually stated on Banach spaces, but it holds without completeness.

The Banach ideal of absolutely summing operators

noncomputable def TauCeti.summingGauge (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (p : ENNReal) [Fact (1 ≤ p)] (E : Type u_2) (F : Type u_3) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : OperatorGauge 𝕜 E F

The p-summing gauge πₚ as an operator gauge.

@[simp]

theorem TauCeti.summingGauge_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : (summingGauge 𝕜 p E F) T = ContinuousLinearMap.summingENorm p T

@[simp]

theorem TauCeti.finiteSubmodule_summingGauge {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : (summingGauge 𝕜 p E F).finiteSubmodule = absolutelySummingOperators 𝕜 p E F

The operators of finite p-summing gauge are the absolutely p-summing operators.

theorem TauCeti.lowerSemicontinuous_summingGauge {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : LowerSemicontinuous ⇑(summingGauge 𝕜 p E F)

The p-summing gauge is lower semicontinuous for the operator-norm topology.

@[reducible, inline]

abbrev TauCeti.AbsolutelySumming (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (p : ENNReal) [Fact (1 ≤ p)] (E : Type u_2) (F : Type u_3) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Type (max u_2 u_3)

The operator ideal Πₚ(E, F) of absolutely p-summing operators, normed by the p-summing norm πₚ. It is a Banach space when F is complete, and its inclusion OperatorGauge.Carrier.toContinuousLinearMapL into the bounded operators is a contraction.

theorem TauCeti.AbsolutelySumming.toContinuousLinearMap_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : AbsolutelySumming 𝕜 p E F) : T.toContinuousLinearMap ∈ absolutelySummingOperators 𝕜 p E F

The underlying operators of Πₚ(E, F) are the absolutely p-summing operators.

def TauCeti.AbsolutelySumming.mk' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T ∈ absolutelySummingOperators 𝕜 p E F) : AbsolutelySumming 𝕜 p E F

An absolutely p-summing operator as an element of Πₚ(E, F).

@[simp]

theorem TauCeti.AbsolutelySumming.toContinuousLinearMap_mk' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T ∈ absolutelySummingOperators 𝕜 p E F) : (mk' hT).toContinuousLinearMap = T

def TauCeti.AbsolutelySumming.smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : StrongDual 𝕜 E) (y : F) : AbsolutelySumming 𝕜 p E F

The rank-one operator x ↦ f x • y in Πₚ(E, F).

@[simp]

theorem TauCeti.AbsolutelySumming.toContinuousLinearMap_smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : StrongDual 𝕜 E) (y : F) : (smulRight f y).toContinuousLinearMap = ContinuousLinearMap.smulRight f y

instance TauCeti.AbsolutelySumming.instCompleteSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] : CompleteSpace (AbsolutelySumming 𝕜 p E F)

Πₚ(E, F) is a Banach space when F is complete.

theorem TauCeti.AbsolutelySumming.norm_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : AbsolutelySumming 𝕜 p E F) : ‖T‖ = (ContinuousLinearMap.summingENorm p T.toContinuousLinearMap).toReal

The norm of Πₚ(E, F) is the p-summing norm.

theorem TauCeti.AbsolutelySumming.enorm_eq_summingENorm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : AbsolutelySumming 𝕜 p E F) : ‖T‖ₑ = ContinuousLinearMap.summingENorm p T.toContinuousLinearMap

The extended norm of Πₚ(E, F) is the p-summing gauge.

theorem TauCeti.AbsolutelySumming.norm_toLp_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : AbsolutelySumming 𝕜 p E F) {ι : Type u_5} [Fintype ι] (x : ι → E) : ‖WithLp.toLp p fun (i : ι) => T.toContinuousLinearMap (x i)‖ ≤ ‖T‖ * (weakLpNorm p) x

The defining inequality of absolutely p-summing operators holds with constant the norm of Πₚ(E, F).

theorem TauCeti.AbsolutelySumming.norm_le_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : AbsolutelySumming 𝕜 p E F} {C : ℝ} (hC : 0 ≤ C) : ‖T‖ ≤ C ↔ ∀ (n : ℕ) (x : Fin n → E), ‖WithLp.toLp p fun (i : Fin n) => T.toContinuousLinearMap (x i)‖ ≤ C * (weakLpNorm p) x

The norm of Πₚ(E, F) is the least constant in the defining inequality.

@[simp]

theorem TauCeti.AbsolutelySumming.norm_smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : StrongDual 𝕜 E) (y : F) : ‖smulRight f y‖ = ‖f‖ * ‖y‖

The rank-one operator x ↦ f x • y has p-summing norm ‖f‖ ‖y‖.

noncomputable def TauCeti.AbsolutelySumming.postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (p : ENNReal) [Fact (1 ≤ p)] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (A : F →L[𝕜] G) : AbsolutelySumming 𝕜 p E F →L[𝕜] AbsolutelySumming 𝕜 p E G

Composition on the left with a bounded operator, as a bounded linear map Πₚ(E, F) → Πₚ(E, G) of norm at most ‖A‖.

@[simp]

theorem TauCeti.AbsolutelySumming.toContinuousLinearMap_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (A : F →L[𝕜] G) (T : AbsolutelySumming 𝕜 p E F) : ((postcomp p E A) T).toContinuousLinearMap = A ∘SL T.toContinuousLinearMap

theorem TauCeti.AbsolutelySumming.norm_postcomp_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (A : F →L[𝕜] G) : ‖postcomp p E A‖ ≤ ‖A‖

Composition on the left multiplies the p-summing norm by at most ‖A‖.

noncomputable def TauCeti.AbsolutelySumming.precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (p : ENNReal) [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (F : Type u_4) [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D : Type u_6} [SeminormedAddCommGroup D] [NormedSpace 𝕜 D] (B : D →L[𝕜] E) : AbsolutelySumming 𝕜 p E F →L[𝕜] AbsolutelySumming 𝕜 p D F

Composition on the right with a bounded operator, as a bounded linear map Πₚ(E, F) → Πₚ(D, F) of norm at most ‖B‖.

@[simp]

theorem TauCeti.AbsolutelySumming.toContinuousLinearMap_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D : Type u_6} [SeminormedAddCommGroup D] [NormedSpace 𝕜 D] (B : D →L[𝕜] E) (T : AbsolutelySumming 𝕜 p E F) : ((precomp p F B) T).toContinuousLinearMap = T.toContinuousLinearMap ∘SL B

theorem TauCeti.AbsolutelySumming.norm_precomp_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D : Type u_6} [SeminormedAddCommGroup D] [NormedSpace 𝕜 D] (B : D →L[𝕜] E) : ‖precomp p F B‖ ≤ ‖B‖

Composition on the right multiplies the p-summing norm by at most ‖B‖.

noncomputable def TauCeti.AbsolutelySumming.inclusion (𝕜 : Type u_1) [RCLike 𝕜] {p : ENNReal} [Fact (1 ≤ p)] (E : Type u_2) (F : Type u_3) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {q : ENNReal} [Fact (1 ≤ q)] (hpq : p ≤ q) : AbsolutelySumming 𝕜 p E F →L[𝕜] AbsolutelySumming 𝕜 q E F

The inclusion Πₚ(E, F) → Π_q(E, F) for p ≤ q, as a contraction.

@[simp]

theorem TauCeti.AbsolutelySumming.toContinuousLinearMap_inclusion {𝕜 : Type u_1} [RCLike 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {q : ENNReal} [Fact (1 ≤ q)] (hpq : p ≤ q) (T : AbsolutelySumming 𝕜 p E F) : ((inclusion 𝕜 E F hpq) T).toContinuousLinearMap = T.toContinuousLinearMap

theorem TauCeti.AbsolutelySumming.norm_inclusion_le {𝕜 : Type u_1} [RCLike 𝕜] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {q : ENNReal} [Fact (1 ≤ q)] (hpq : p ≤ q) : ‖inclusion 𝕜 E F hpq‖ ≤ 1

The inclusion Πₚ(E, F) → Π_q(E, F) is a contraction.