Continuous functions on weak-star dual balls

Banach–Alaoglu makes every closed dual ball compact in the weak-star topology. The norm of evaluation, raised to a nonnegative exponent, is a continuous real-valued function on such a ball. This bundled function supplies the integrand in Pietsch domination.

Evaluation at a vector is itself a continuous function on such a ball, and WeakDual.evalClosedBall bundles x ↦ (φ ↦ φ x) as a bounded operator from E into the continuous functions on the ball of radius r, of norm at most r. On the unit ball it is the canonical map of E into C(B, 𝕜) through which Pietsch factorization passes to Lᵖ.

instance WeakDual.instCompactSpaceElemPreimageStrongDualCoeLinearEquivIdToStrongDualClosedBallOfProperSpace_tauCeti {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] (f : StrongDual 𝕜 E) (r : ℝ) : CompactSpace ↑(⇑toStrongDual ⁻¹' Metric.closedBall f r)

A closed dual ball, with its weak-star topology, is compact by Banach–Alaoglu.

noncomputable def WeakDual.evalRpow {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : ℝ) (p : ENNReal) (x : E) : C(↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 r), ℝ)

The continuous function φ ↦ ‖φ x‖ ^ p on the weak-star closed ball of radius r.

@[simp]

theorem WeakDual.evalRpow_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : ℝ) (p : ENNReal) (x : E) (φ : ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 r)) : (evalRpow r p x) φ = ‖↑φ x‖ ^ p.toReal

noncomputable def WeakDual.evalClosedBall {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] (r : ℝ) : E →L[𝕜] C(↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 r), 𝕜)

Evaluation x ↦ (φ ↦ φ x), as a bounded operator from E into the continuous functions on the weak-star closed dual ball of radius r.

@[simp]

theorem WeakDual.evalClosedBall_apply_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] (r : ℝ) (x : E) (φ : ↑(⇑toStrongDual ⁻¹' Metric.closedBall 0 r)) : ((evalClosedBall r) x) φ = ↑φ x

theorem WeakDual.norm_evalClosedBall_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] {r : ℝ} (hr : 0 ≤ r) : ‖evalClosedBall r‖ ≤ r

Evaluation on the dual ball of radius r ≥ 0 has operator norm at most r.