The force curve of the forced regularized construction

A locally square-integrable force has a strongly measurable modification on positive times; its time slices form a strongly measurable curve of L² fields whose squared norms are integrable on bounded time intervals. This is the force entering the Duhamel term of eq:reg-mild-forced.

theorem CKN.Leray.exists_forcedForceModification {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : ∃ (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3), MeasureTheory.StronglyMeasurable F ∧ ∀ (T : ℝ), 0 < T → ∀ᵐ (z : Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)), F z = f z

noncomputable def CKN.Leray.forcedForceMod (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

A strongly measurable modification of a locally square-integrable force.

Equations

• CKN.Leray.forcedForceMod f hf = Classical.choose ⋯

theorem CKN.Leray.forcedForceMod_stronglyMeasurable (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) : MeasureTheory.StronglyMeasurable (forcedForceMod f hf)

theorem CKN.Leray.forcedForceMod_ae_eq (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) {T : ℝ} (hT : 0 < T) : ∀ᵐ (z : Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)), forcedForceMod f hf z = f z

theorem CKN.Leray.realVectorL2OfCoordinateFunction_ae_eq_toLp (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : ↑↑(realVectorL2OfCoordinateFunction a ha) =ᵐ[MeasureTheory.volume] fun (y : Foundation.Parabolic.L2Vec3) => WithLp.toLp 2 (a y.ofLp)

The class of a square-integrable coordinate field agrees on the Euclidean carrier with the transferred field.

theorem CKN.Leray.forcedForceSlice_stronglyMeasurable {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) : MeasureTheory.StronglyMeasurable (forcedForceSlice F)

The force slice curve of a strongly measurable field is strongly measurable.

theorem CKN.Leray.norm_forcedForceSlice_le (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (s : ℝ) : ‖forcedForceSlice F s‖ ≤ 2 * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, s)) 2 MeasureTheory.volume).toReal

theorem CKN.Leray.memLp_forcedForceMod_prod (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) {T : ℝ} (hT : 0 < T) : MeasureTheory.MemLp (forcedForceMod f hf) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

The strongly measurable modification is square integrable on every positive-time slab.

theorem CKN.Leray.integrableOn_forcedForceSlice_sq (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (T : ℝ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖forcedForceSlice (forcedForceMod f hf) s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume

The squared norms of the force curve are integrable on bounded time intervals.