Pietsch factorization

Let 1 ≤ p < ∞ and let B be the closed unit ball of the dual of E, with its weak-star topology. For a finite Borel measure ν on B, evaluation gives the canonical operator jₚ : E →L[𝕜] Lᵖ(ν), x ↦ (f ↦ f x), written WeakDual.evalLp p ν; its norm at x is (∫ |f x|ᵖ dν(f))^(1/p), and it is a contraction when ν is a probability measure.

In these terms, Pietsch domination says that πₚ(T) ≤ C exactly when ‖T x‖ ≤ C ‖jₚ x‖ for some regular Borel probability measure ν on B. Such a bound is the same as a factorization of T through jₚ:

• for any normed target F, πₚ(T) ≤ C iff T = S ∘ jₚ for some ν and some operator S of norm at most C on the canonical image range jₚ ⊆ Lᵖ(ν);
• for a Banach target F, πₚ(T) ≤ C iff the same holds with S defined on the closure of range jₚ in Lᵖ(ν).

Main declarations

• WeakDual.evalLp: the canonical operator jₚ : E →L[𝕜] Lᵖ(ν).
• WeakDual.norm_evalLp_apply: ‖jₚ x‖ = (∫ |f x|ᵖ dν(f))^(1/p).
• ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_norm_le_mul_norm_evalLp: Pietsch domination stated with jₚ.
• ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_rangeRestrict: Pietsch factorization through the canonical image.
• ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_codRestrict_topologicalClosure: Pietsch factorization through the closure of the canonical image, for a Banach target.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, Theorem 8.2.8.
• J. Diestel, H. Jarchow and A. Tonge, Absolutely Summing Operators, Theorem 2.13.

noncomputable def WeakDual.evalLp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] (p : ENNReal) [Fact (1 ≤ p)] (ν : MeasureTheory.Measure ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 1)) [MeasureTheory.IsFiniteMeasure ν] : E →L[𝕜] ↥(MeasureTheory.Lp 𝕜 p ν)

The canonical operator jₚ : E →L[𝕜] Lᵖ(ν) sending x to the class of f ↦ f x, for a finite measure ν on the weak-star closed unit ball of the dual.

theorem WeakDual.coeFn_evalLp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal} [Fact (1 ≤ p)] (ν : MeasureTheory.Measure ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 1)) [MeasureTheory.IsFiniteMeasure ν] (x : E) : ↑↑((evalLp p ν) x) =ᵐ[ν] fun (f : ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 1)) => ↑f x

The canonical operator jₚ sends x to the class of the evaluation f ↦ f x.

theorem WeakDual.norm_evalLp_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal} [Fact (1 ≤ p)] (ν : MeasureTheory.Measure ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 1)) [MeasureTheory.IsFiniteMeasure ν] (hp : p ≠ ⊤) (x : E) : ‖(evalLp p ν) x‖ = (∫ (f : ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 1)), ‖↑f x‖ ^ p.toReal ∂ν) ^ (1 / p.toReal)

The Lᵖ norm of jₚ x is (∫ |f x|ᵖ dν(f))^(1/p).

theorem WeakDual.norm_evalLp_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal} [Fact (1 ≤ p)] (ν : MeasureTheory.Measure ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 1)) [MeasureTheory.IsProbabilityMeasure ν] : ‖evalLp p ν‖ ≤ 1

For a probability measure ν, the canonical operator jₚ is a contraction.

theorem ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_norm_le_mul_norm_evalLp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal} [Fact (1 ≤ p)] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (hp : p ≠ ⊤) {T : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) : summingENorm p T ≤ ENNReal.ofReal C ↔ ∃ (ν : MeasureTheory.Measure ↑(⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)) (x : MeasureTheory.IsProbabilityMeasure ν), ν.Regular ∧ ∀ (x_1 : E), ‖T x_1‖ ≤ C * ‖(WeakDual.evalLp p ν) x_1‖

Pietsch domination in terms of the canonical operator jₚ : E →L[𝕜] Lᵖ(ν): for 1 ≤ p < ∞ and C ≥ 0, πₚ(T) ≤ C iff ‖T x‖ ≤ C ‖jₚ x‖ for all x, for some regular Borel probability measure ν on the weak-star compact dual unit ball.

theorem ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_rangeRestrict {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal} [Fact (1 ≤ p)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (hp : p ≠ ⊤) {T : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) : summingENorm p T ≤ ENNReal.ofReal C ↔ ∃ (ν : MeasureTheory.Measure ↑(⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)) (x : MeasureTheory.IsProbabilityMeasure ν), ν.Regular ∧ ∃ (S : ↥(↑(WeakDual.evalLp p ν)).range →L[𝕜] F), ‖S‖ ≤ C ∧ T = S ∘SL (WeakDual.evalLp p ν).rangeRestrict

Pietsch factorization through the canonical image: for 1 ≤ p < ∞ and C ≥ 0, πₚ(T) ≤ C iff there are a regular Borel probability measure ν on the weak-star compact dual unit ball and an operator S of norm at most C on the canonical image range jₚ ⊆ Lᵖ(ν) such that T = S ∘ jₚ.

theorem ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_codRestrict_topologicalClosure {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal} [Fact (1 ≤ p)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (hp : p ≠ ⊤) {T : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) : summingENorm p T ≤ ENNReal.ofReal C ↔ ∃ (ν : MeasureTheory.Measure ↑(⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)) (x : MeasureTheory.IsProbabilityMeasure ν), ν.Regular ∧ ∃ (S : ↥(↑(WeakDual.evalLp p ν)).range.topologicalClosure →L[𝕜] F), ‖S‖ ≤ C ∧ T = S ∘SL (WeakDual.evalLp p ν).codRestrict (↑(WeakDual.evalLp p ν)).range.topologicalClosure ⋯

Pietsch factorization through the closure of the canonical image: for a Banach space F, 1 ≤ p < ∞ and C ≥ 0, πₚ(T) ≤ C iff there are a regular Borel probability measure ν on the weak-star compact dual unit ball and an operator S of norm at most C on the closure of range jₚ in Lᵖ(ν) such that T = S ∘ jₚ.