Weakly measurable functions into a separable Hilbert space

A function h : α → E into an inner product space is weakly measurable when every scalar function t ↦ ⟪v, h t⟫ is measurable. Pettis' measurability theorem says that a weakly measurable function with essentially separable range is strongly measurable. This file proves the case of a separable inner product space E, with almost everywhere strong measurability on both sides:

• TauCeti.aestronglyMeasurable_iff_forall_inner: h : α → E is almost everywhere strongly measurable exactly when each t ↦ ⟪v, h t⟫ is;
• TauCeti.aestronglyMeasurable_strongDual_iff_forall_apply: for E also complete, a function g : α → StrongDual 𝕜 E is almost everywhere strongly measurable in the operator norm exactly when each t ↦ g t v is;
• MeasureTheory.MemLp.clm_apply_of_forall_aestronglyMeasurable: if A t : F →L[𝕜] E* is essentially bounded and weakly measurable, t ↦ A t x y measurable for all x, y, then t ↦ A t (u t) lies in Lᵖ(E*) for every u ∈ Lᵖ(F).

The last statement is what evolution equations need. A time-dependent operator A(t) : V →L[ℝ] V* with merely measurable coefficients is in general only weakly measurable, and not measurable for the operator norm, but for a separable Hilbert space V, such as H¹₀(Ω), and u ∈ L²(0, T; V), the function t ↦ A(t) u(t) is a genuine element of L²(0, T; V*).

Proof

Let U n be the span of the first n + 1 terms of a dense sequence in E. The orthogonal projection onto U n is a finite sum ∑ i, ⟪b i, x⟫ • b i over an orthonormal basis b of U n, so t ↦ P_{U n} (h t) is almost everywhere strongly measurable, and it converges to h t because the U n increase to a dense subspace (Submodule.starProjection_tendsto_self). The dual statement follows through the Riesz isometry InnerProductSpace.toDual.

References

• B. J. Pettis, On integration in vector spaces, Trans. Amer. Math. Soc. 44 (1938), 277–304.
• J. Diestel, J. J. Uhl, Vector Measures, Mathematical Surveys 15, AMS, 1977, Chapter II, §1, Theorem 2.

theorem TauCeti.aestronglyMeasurable_iff_forall_inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] {h : α → E} : MeasureTheory.AEStronglyMeasurable h μ ↔ ∀ (v : E), MeasureTheory.AEStronglyMeasurable (fun (t : α) => inner 𝕜 v (h t)) μ

Pettis' theorem in a separable inner product space. A function into a separable inner product space is almost everywhere strongly measurable exactly when it is weakly measurable, that is, when each of its coordinates t ↦ ⟪v, h t⟫ is almost everywhere strongly measurable.

theorem TauCeti.aestronglyMeasurable_strongDual_iff_forall_apply {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] [CompleteSpace E] {g : α → StrongDual 𝕜 E} : MeasureTheory.AEStronglyMeasurable g μ ↔ ∀ (v : E), MeasureTheory.AEStronglyMeasurable (fun (t : α) => (g t) v) μ

Pettis' theorem for the dual of a separable Hilbert space. A function into the dual of a separable Hilbert space is almost everywhere strongly measurable in the operator norm exactly when each of its evaluations t ↦ g t v is almost everywhere strongly measurable.

theorem MeasureTheory.MemLp.clm_apply_of_forall_aestronglyMeasurable {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {x✝ : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} {u : α → F} {A : α → F →L[𝕜] StrongDual 𝕜 E} {Λ : ℝ} (hu : MemLp u p μ) (hA : ∀ (x : F) (y : E), AEStronglyMeasurable (fun (t : α) => ((A t) x) y) μ) (hA_bound : ∀ᵐ (t : α) ∂μ, ‖A t‖ ≤ Λ) : MemLp (fun (t : α) => (A t) (u t)) p μ

Weakly measurable operator families act on Lᵖ. Let E be a separable Hilbert space and let A t : F →L[𝕜] E* be essentially bounded by Λ and weakly measurable: t ↦ A t x y is almost everywhere strongly measurable for all x, y. Then t ↦ A t (u t) lies in Lᵖ(E*) for every u ∈ Lᵖ(F).