Measurability of Carathéodory compositions

Let g : α → X → G be a Carathéodory function: t ↦ g t x is almost everywhere strongly measurable for each x and x ↦ g t x is continuous for almost every t. Then t ↦ g t (u t) is almost everywhere strongly measurable for every almost everywhere strongly measurable u : α → X (MeasureTheory.AEStronglyMeasurable.apply_of_forall_of_continuousAt); in fact continuity of g t at the point u t suffices. When G is second countable, for instance for a real-valued g, measurability of each section t ↦ g t x already implies the measurability hypothesis.

No separability or metrizability is asked of X: u is approximated by simple functions s, on whose finitely many fibres t ↦ g t (s t) is one of the sections t ↦ g t x. This is what weak measurability of a time-dependent operator A(t) : V →L[ℝ] V* in parabolic problems needs: t ↦ A(t) u(t) φ(t) is measurable as soon as t ↦ A(t) u v is for all fixed u, v, for an arbitrary Hilbert space V. Mathlib's stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable proves joint measurability instead, which needs a second-countable metrizable parameter space.

theorem MeasureTheory.AEStronglyMeasurable.apply_of_forall_of_continuousAt {α : Type u_1} {X : Type u_2} {G : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace X] [TopologicalSpace G] [TopologicalSpace.PseudoMetrizableSpace G] {u : α → X} (hu : AEStronglyMeasurable u μ) {g : α → X → G} (hg : ∀ (x : X), AEStronglyMeasurable (fun (t : α) => g t x) μ) (hg_cont : ∀ᵐ (t : α) ∂μ, ContinuousAt (g t) (u t)) : AEStronglyMeasurable (fun (t : α) => g t (u t)) μ

Carathéodory composition. If t ↦ g t x is almost everywhere strongly measurable for every x and g t is continuous at u t for almost every t, then t ↦ g t (u t) is almost everywhere strongly measurable for every almost everywhere strongly measurable u.