Jointly measurable representatives of L²-valued curves

The regularized construction of lem:regularised-forced works with curves of square-integrable fields. To compute with them pointwise, a strongly measurable curve s ↦ γ s ∈ L²(μ) is represented by one jointly measurable function Γ(x, s) whose slices are the classes γ s. The Bochner integral of such a curve is then computed pointwise almost everywhere by integrating the representative in the curve variable.

theorem CKN.Leray.exists_jointRep_of_stronglyMeasurable {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] [Nonempty E] (γ : β → ↥(MeasureTheory.Lp E 2 μ)) (hγ : MeasureTheory.StronglyMeasurable γ) : ∃ (Γ : α × β → E), MeasureTheory.StronglyMeasurable Γ ∧ ∀ (s : β), (fun (x : α) => Γ (x, s)) =ᵐ[μ] ↑↑(γ s)

A strongly measurable curve of L² classes has a jointly strongly measurable representative whose every slice is the class of the curve.

theorem CKN.Leray.exists_jointRep_of_aestronglyMeasurable {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] [Nonempty E] {ν : MeasureTheory.Measure β} (γ : β → ↥(MeasureTheory.Lp E 2 μ)) (hγ : MeasureTheory.AEStronglyMeasurable γ ν) : ∃ (Γ : α × β → E), MeasureTheory.StronglyMeasurable Γ ∧ ∀ᵐ (s : β) ∂ν, (fun (x : α) => Γ (x, s)) =ᵐ[μ] ↑↑(γ s)

An almost everywhere strongly measurable curve of L² classes has a jointly strongly measurable representative whose slices are the classes of the curve for almost every value of the curve variable.

theorem CKN.Leray.setIntegral_norm_le_sqrt_measure_mul_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E 2 μ)) {B : Set α} (hμB : μ B < ⊤) : ∫ (x : α) in B, ‖↑↑f x‖ ∂μ ≤ (μ B).toReal ^ (1 / 2) * ‖f‖

On a set of finite measure, the integral of the norm of an L² class is bounded by the square root of the measure times its L² norm.

theorem CKN.Leray.integrable_jointRep_restrict_prod {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasureTheory.SFinite μ] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (γ : β → ↥(MeasureTheory.Lp E 2 μ)) (hγ : MeasureTheory.Integrable γ ν) (Γ : α × β → E) (hΓ : MeasureTheory.StronglyMeasurable Γ) (hrep : ∀ᵐ (s : β) ∂ν, (fun (x : α) => Γ (x, s)) =ᵐ[μ] ↑↑(γ s)) {B : Set α} (hμB : μ B < ⊤) : MeasureTheory.Integrable Γ ((μ.restrict B).prod ν)

The representative of an integrable curve is integrable on the product of a finite-measure set with the curve measure.

theorem CKN.Leray.integral_ae_eq_integral_jointRep {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [CompleteSpace E] [MeasureTheory.SigmaFinite μ] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (γ : β → ↥(MeasureTheory.Lp E 2 μ)) (hγ : MeasureTheory.Integrable γ ν) (Γ : α × β → E) (hΓ : MeasureTheory.StronglyMeasurable Γ) (hrep : ∀ᵐ (s : β) ∂ν, (fun (x : α) => Γ (x, s)) =ᵐ[μ] ↑↑(γ s)) : ↑↑(∫ (s : β), γ s ∂ν) =ᵐ[μ] fun (x : α) => ∫ (s : β), Γ (x, s) ∂ν

The Bochner integral of an integrable curve of L² classes is computed almost everywhere by integrating a jointly measurable representative in the curve variable.