Weak Lᵖ norms of finite families

For a finite family x : ι → E over real or complex scalars, its weak Lᵖ norm is the supremum of the Lᵖ norms of (f (x i))ᵢ over the closed unit ball of the continuous dual. It is the operator norm of the dual-evaluation map into PiLp, so it is finite without completeness or finite dimensionality assumptions on E.

weakLpNorm is bundled as a Seminorm, providing homogeneity and the triangle inequality through the existing seminorm API. Over real or complex scalars it dominates each coordinate norm, and is therefore a norm on finite families in a normed space. We prove the bound on sums of p-th powers of scalar evaluations, the strong Lᵖ bound, invariance under reindexing, the bounded-operator estimate, the exact value on scalar multiples of one vector, its agreement with the strong norm at exponent ∞, and Hölder's inequality for scalar weights: the weak p-norm of (cᵢ xᵢ)ᵢ is at most ‖c‖ₛ times the weak q-norm of x when 1 / p = 1 / s + 1 / q. These are the finite-family estimates used for absolutely summing operators.

The weak norm is continuous, being dominated by the strong norm. At exponent 1 it is the least upper bound for the norms ‖∑ i, c i • x i‖ over scalar coefficients of norm at most one, and it controls unconditional summability. The finite subfamilies of an unconditionally summable family have uniformly bounded weak L¹ norms, by the uniform boundedness principle on the complete dual. Conversely, in a complete space, finite blocks whose weak L¹ norms are summable assemble into an unconditionally summable family; in any space, these blocks, each followed by its negative, form a family summing to zero.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, Chapter 8.

The construction uses Mathlib's inclusionInDoubleDual and PiLp; the supremum formula uses ContinuousLinearMap.sSup_unitClosedBall_eq_norm, and the uniform bound for summable families uses banach_steinhaus.

noncomputable def TauCeti.dualEvalLp {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] : (ι → E) →ₗ[𝕜] StrongDual 𝕜 E →L[𝕜] PiLp p fun (x : ι) => 𝕜

Send a finite vector family to its dual-evaluation operator with Lᵖ target norm.

@[simp]

theorem TauCeti.dualEvalLp_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) (f : StrongDual 𝕜 E) : ((dualEvalLp p) x) f = WithLp.toLp p fun (i : ι) => f (x i)

Dual evaluation is the family of scalar evaluations, viewed in PiLp.

noncomputable def TauCeti.weakLpNorm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] : Seminorm 𝕜 (ι → E)

The weak Lᵖ seminorm of a finite family is the norm of its dual-evaluation operator.

theorem TauCeti.weakLpNorm_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) : (weakLpNorm p) x = ‖(dualEvalLp p) x‖

The operator-norm characterization of the weak Lᵖ seminorm.

theorem TauCeti.norm_eval_le_weakLpNorm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) (f : StrongDual 𝕜 E) : ‖WithLp.toLp p fun (i : ι) => f (x i)‖ ≤ (weakLpNorm p) x * ‖f‖

Scalar evaluations are bounded by the weak Lᵖ norm times the functional norm.

theorem TauCeti.sum_norm_eval_rpow_le_weakLpNorm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (hp : p ≠ ⊤) (x : ι → E) (f : StrongDual 𝕜 E) : ∑ i : ι, ‖f (x i)‖ ^ p.toReal ≤ ((weakLpNorm p) x * ‖f‖) ^ p.toReal

For finite p, the p-th powers of scalar evaluations sum to at most the p-th power of the weak Lᵖ norm times the functional norm.

theorem TauCeti.weakLpNorm_le_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) {C : ℝ} (hC : 0 ≤ C) : (weakLpNorm p) x ≤ C ↔ ∀ (f : StrongDual 𝕜 E), ‖WithLp.toLp p fun (i : ι) => f (x i)‖ ≤ C * ‖f‖

An upper bound on the weak norm is equivalent to the homogeneous evaluation bound.

theorem TauCeti.weakLpNorm_le_norm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) : (weakLpNorm p) x ≤ ‖WithLp.toLp p x‖

The weak Lᵖ norm is at most the strong Lᵖ norm of the vector family.

theorem TauCeti.weakLpNorm_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (T : E →L[𝕜] F) (x : ι → E) : (weakLpNorm p) (⇑T ∘ x) ≤ ‖T‖ * (weakLpNorm p) x

Applying a bounded operator to a family multiplies its weak norm by at most the operator norm.

theorem TauCeti.weakLpNorm_comp_equiv {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] {κ : Type u_5} [Fintype κ] (e : κ ≃ ι) (x : ι → E) : (weakLpNorm p) (x ∘ ⇑e) = (weakLpNorm p) x

Reindexing a finite family by an equivalence preserves its weak Lᵖ norm.

theorem TauCeti.continuous_weakLpNorm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] : Continuous ⇑(weakLpNorm p)

The weak Lᵖ norm is continuous, being dominated by the strong Lᵖ norm.

theorem TauCeti.weakLpNorm_smul_le {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] {q : ENNReal} [Fact (1 ≤ q)] {s : ℝ} (hspq : s.HolderTriple q.toReal p.toReal) (c : ι → 𝕜) (x : ι → E) : ((weakLpNorm p) fun (i : ι) => c i • x i) ≤ (∑ i : ι, ‖c i‖ ^ s) ^ (1 / s) * (weakLpNorm q) x

Hölder's inequality for weak norms. Multiplying a finite family by scalar weights c multiplies its weak norm by at most the ℓˢ norm of the weights, when 1 / p = 1 / s + 1 / q with finite p and q.

theorem TauCeti.weakLpNorm_eq_sSup {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [DenselyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) : (weakLpNorm p) x = sSup ((fun (f : StrongDual 𝕜 E) => ‖WithLp.toLp p fun (i : ι) => f (x i)‖) '' Metric.closedBall 0 1)

The weak Lᵖ norm is the supremum of scalar Lᵖ evaluations over the dual unit ball.

theorem TauCeti.weakLpNorm_le_iff_unitBall {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [DenselyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) {C : ℝ} : (weakLpNorm p) x ≤ C ↔ ∀ (f : StrongDual 𝕜 E), ‖f‖ ≤ 1 → ‖WithLp.toLp p fun (i : ι) => f (x i)‖ ≤ C

Bounding the weak norm is equivalent to bounding evaluations on the dual unit ball.

theorem TauCeti.norm_le_weakLpNorm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) (i : ι) : ‖x i‖ ≤ (weakLpNorm p) x

Each coordinate norm is at most the weak norm of the whole family.

theorem TauCeti.weakLpNorm_smul_const {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (a : ι → 𝕜) (v : E) : ((weakLpNorm p) fun (i : ι) => a i • v) = ‖WithLp.toLp p a‖ * ‖v‖

A family of multiples of one vector has weak norm equal to its scalar Lᵖ norm times the vector norm. This includes the one-coordinate normalization.

@[simp]

theorem TauCeti.weakLpNorm_single {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] [DecidableEq ι] (i : ι) (v : E) : (weakLpNorm p) (Pi.single i v) = ‖v‖

A family supported at a single coordinate has weak norm equal to that vector's norm.

@[simp]

theorem TauCeti.weakLpNorm_top {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (x : ι → E) : (weakLpNorm ⊤) x = ‖WithLp.toLp ⊤ x‖

At exponent ∞ the weak norm of a finite family is its strong norm, the largest norm of its members.

theorem TauCeti.norm_sum_smul_le_weakLpNorm_one {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (x : ι → E) {c : ι → 𝕜} (hc : ∀ (i : ι), ‖c i‖ ≤ 1) : ‖∑ i : ι, c i • x i‖ ≤ (weakLpNorm 1) x

A combination of a finite family with scalar coefficients of norm at most one has norm at most the weak L¹ norm of the family.

theorem TauCeti.weakLpNorm_one_le_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (x : ι → E) {C : ℝ} : (weakLpNorm 1) x ≤ C ↔ ∀ (c : ι → 𝕜), (∀ (i : ι), ‖c i‖ ≤ 1) → ‖∑ i : ι, c i • x i‖ ≤ C

The weak L¹ norm by bounded coefficients. The weak L¹ norm of a finite family is the least upper bound for the norms of its combinations with scalar coefficients of norm at most one.

theorem Summable.exists_forall_weakLpNorm_one_le {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {x : ι → E} (hx : Summable x) : ∃ (C : ℝ), ∀ (s : Finset ι), ((TauCeti.weakLpNorm 1) fun (i : ↥s) => x ↑i) ≤ C

The finite subfamilies of an unconditionally summable family have uniformly bounded weak L¹ norms.

theorem TauCeti.summable_sigma_of_summable_weakLpNorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {κ : Type u_4} {β : κ → Type u_5} [(k : κ) → Fintype (β k)] {y : (k : κ) → β k → E} (hy : Summable fun (k : κ) => (weakLpNorm 1) (y k)) : Summable fun (j : (k : κ) × β k) => y j.fst j.snd

In a complete space, finite blocks whose weak L¹ norms are summable assemble into an unconditionally summable family.

theorem TauCeti.hasSum_elim_neg_zero_of_summable_weakLpNorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {κ : Type u_4} {β : κ → Type u_5} [(k : κ) → Fintype (β k)] {y : (k : κ) → β k → E} (hy : Summable fun (k : κ) => (weakLpNorm 1) (y k)) : HasSum (Sum.elim (fun (j : (k : κ) × β k) => y j.fst j.snd) fun (j : (k : κ) × β k) => -y j.fst j.snd) 0

Finite blocks whose weak L¹ norms are summable, each followed by its negative, form a family summing to zero, even when E is not complete.

@[simp]

theorem TauCeti.weakLpNorm_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal) [Fact (1 ≤ p)] (x : ι → E) : (weakLpNorm p) x = 0 ↔ x = 0

The weak Lᵖ seminorm separates finite families over real or complex scalars.