Measurable curves of L² classes from jointly measurable fields #
A jointly measurable field Γ(x, s) with square-integrable slices defines a
curve s ↦ [Γ(·, s)] of L² classes. Its distance to any fixed class is a
measurable function of s by Tonelli, and in a separable metric space this
already makes the curve measurable. This is the measurability used for the
force and Stokes Duhamel integrands of lem:regularised-forced.
theorem
CKN.Leray.measurable_of_measurable_dist
{β : Type u_1}
{Y : Type u_2}
[MeasurableSpace β]
[PseudoMetricSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[TopologicalSpace.SeparableSpace Y]
{f : β → Y}
(hf : ∀ (y : Y), Measurable fun (s : β) => dist (f s) y)
:
In a separable pseudometric Borel space, a map whose distances to all points are measurable is measurable.
theorem
CKN.Leray.measurable_dist_slice_class
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.SFinite μ]
(Γ : α × β → E)
(hΓ : MeasureTheory.StronglyMeasurable Γ)
(γ : β → ↥(MeasureTheory.Lp E 2 μ))
(hrep : ∀ (s : β), (fun (x : α) => Γ (x, s)) =ᵐ[μ] ↑↑(γ s))
(c : ↥(MeasureTheory.Lp E 2 μ))
:
Measurable fun (s : β) => dist (γ s) c
The L² distance from the slices of a jointly measurable field to a fixed
class is measurable in the slice variable.
theorem
CKN.Leray.stronglyMeasurable_of_jointRep
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.SFinite μ]
[MeasurableSpace.CountablyGenerated α]
[SecondCountableTopology E]
(Γ : α × β → E)
(hΓ : MeasureTheory.StronglyMeasurable Γ)
(γ : β → ↥(MeasureTheory.Lp E 2 μ))
(hrep : ∀ (s : β), (fun (x : α) => Γ (x, s)) =ᵐ[μ] ↑↑(γ s))
:
A curve of L² classes represented slice by slice by a jointly measurable
field is strongly measurable.