Integrability on weak-star dual balls

On the weak-star closed dual ball of radius r, every functional φ satisfies ‖φ x‖ ≤ r * ‖x‖, so the continuous function φ ↦ ‖φ x‖ ^ p is bounded. It is therefore integrable against every finite measure on the ball for an opens-measurable structure on the weak dual. These are the integrands of Pietsch domination.

Main results

• MeasureTheory.Measure.integrable_norm_apply_rpow: for a finite measure ν on a weak-star closed dual ball, φ ↦ ‖φ x‖ ^ p is ν-integrable.

theorem MeasureTheory.Measure.integrable_norm_apply_rpow {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [OpensMeasurableSpace (WeakDual 𝕜 E)] {r : ℝ} (ν : Measure ↑(⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 r)) [IsFiniteMeasure ν] (p : ENNReal) (x : E) : Integrable (fun (φ : ↑(⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 r)) => ‖↑φ x‖ ^ p.toReal) ν

For a finite measure on a weak-star closed dual ball, each function φ ↦ ‖φ x‖ ^ p is integrable.