Space-time representatives of the forced regularized solution

A continuous curve of real L² fields has a jointly measurable space-time representative whose every time slice represents the curve. Its weak gradient is represented by the limit of the gradients of spatial mollifications, which is jointly measurable and whose slices are the weak gradients of the slices wherever those exist. These are the velocity and gradient fields of lem:regularised-forced.

theorem CKN.Leray.exists_forcedCurveRep (U : ℝ → ↥RealVectorL2) (hU : MeasureTheory.StronglyMeasurable U) : ∃ (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3), MeasureTheory.StronglyMeasurable u ∧ ∀ (t : ℝ), (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U t)

noncomputable def CKN.Leray.forcedCurveRep (U : ℝ → ↥RealVectorL2) (hU : MeasureTheory.StronglyMeasurable U) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

A jointly measurable space-time representative of a strongly measurable curve of real L² fields, whose time slices represent the curve.

Equations

• CKN.Leray.forcedCurveRep U hU = Classical.choose ⋯

theorem CKN.Leray.forcedCurveRep_stronglyMeasurable (U : ℝ → ↥RealVectorL2) (hU : MeasureTheory.StronglyMeasurable U) : MeasureTheory.StronglyMeasurable (forcedCurveRep U hU)

theorem CKN.Leray.forcedCurveRep_slice (U : ℝ → ↥RealVectorL2) (hU : MeasureTheory.StronglyMeasurable U) (t : ℝ) : (fun (x : Foundation.Parabolic.Vec3) => forcedCurveRep U hU (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U t)

noncomputable def CKN.Leray.forcedMollifiedGrad (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) : ℝ

The gradient field obtained as the limit of the gradients of the spatial mollifications of the slices.

Equations

• CKN.Leray.forcedMollifiedGrad u z i j = Filter.atTop.limUnder fun (n : ℕ) => (fderiv ℝ (CKN.mollify (fun (y : CKN.Vec 3) => u (y, z.2) i) (1 / (↑n + 1)) ⋯) z.1) (CKN.basisVec j)

theorem CKN.Leray.mollify_eq_integral {g : Foundation.Parabolic.Vec3 → ℝ} {δ : ℝ} (hδ : 0 < δ) (x : Foundation.Parabolic.Vec3) : mollify g δ hδ x = ∫ (τ : Vec 3), mollifier δ hδ τ * g (x - τ)

theorem CKN.Leray.measurable_mollify_slice {u : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hu : MeasureTheory.StronglyMeasurable u) {δ : ℝ} (hδ : 0 < δ) (x : Foundation.Parabolic.Vec3) : Measurable fun (t : ℝ) => mollify (fun (y : Vec 3) => u (y, t)) δ hδ x

At a fixed point, the mollification of the slices of a jointly measurable field is measurable in time.

theorem CKN.Leray.forcedMollifiedGrad_stronglyMeasurable {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hu : MeasureTheory.StronglyMeasurable u) (hloc : ∀ (t : ℝ) (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (y : Foundation.Parabolic.Vec3) => u (y, t) i) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.StronglyMeasurable fun (z : Foundation.Parabolic.Vec3 × ℝ) => forcedMollifiedGrad u z i j

The mollified-gradient field of a jointly measurable field with locally integrable slices is jointly measurable.

theorem CKN.Leray.forcedMollifiedGrad_slice_ae_eq {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {t : ℝ} {i j : Fin 3} (hloc : MeasureTheory.LocallyIntegrable (fun (y : Foundation.Parabolic.Vec3) => u (y, t) i) MeasureTheory.volume) {G : Foundation.Parabolic.Vec3 → ℝ} (hG : MeasureTheory.LocallyIntegrable G MeasureTheory.volume) (hweak : HasWeakPartialDerivOn Set.univ j (fun (y : Vec 3) => u (y, t) i) G) : (fun (x : Foundation.Parabolic.Vec3) => forcedMollifiedGrad u (x, t) i j) =ᵐ[MeasureTheory.volume] G

Where a slice has a locally integrable weak partial derivative, the mollified-gradient field represents it.