The space-time form of the forced energy inequality

The slice-wise gradient bounds of the forced regularized solution give, by Tonelli's theorem, the space-time dissipation bound and the square integrability of the gradient field on bounded slabs; the work of the force along the solution curve is the space-time integral of the force against the velocity. These are the space-time forms of eq:reg-energy-forced used in lem:regularised-forced.

theorem CKN.Leray.norm_sq_le_sum_sq_entries (M : Fin 3 → Foundation.Parabolic.Vec3) : ‖M‖ ^ 2 ≤ ∑ i : Fin 3, ∑ j : Fin 3, M i j ^ 2

The squared norm of a matrix is bounded by the sum of its squared entries.

theorem CKN.Leray.measurable_forcedMollifiedGrad {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) : Measurable (forcedMollifiedGrad u)

theorem CKN.Leray.measurable_spatialGradientSq_forcedMollifiedGrad {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) : Measurable fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialGradientSq u (forcedMollifiedGrad u) z

theorem CKN.Leray.forcedSlice_gradient_dissipation {U : ℝ → ↥RealVectorL2} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hrep : ∀ (s : ℝ), (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U s)) {w : ↥ComplexVectorL2} {s : ℝ} (hw : realPartVectorL2 w = U s) (hv : MeasureTheory.MemLp (forcedFourierGradHat w) 2 MeasureTheory.volume) : (∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => forcedMollifiedGrad u (x, s) i) ∧ ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u (forcedMollifiedGrad u) (x, s)) ≤ ENNReal.ofReal (forcedFourierDissipation w)

A time slice whose complex lift has square-integrable frequency gradient has the mollified-gradient field as weak gradient, with squared norm bounded by the frequency dissipation.

theorem CKN.Leray.lintegral_slab_eq_prod (g : Foundation.Parabolic.Vec3 × ℝ → ENNReal) (I : Set ℝ) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ I, g z = ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), g z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict I)

A lower integral over a slab of all space is an integral for the product measure.

theorem CKN.Leray.integral_slab_eq_prod (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (I : Set ℝ) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ I, g z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), g z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict I)

An integral over a slab of all space is an integral for the product measure.

theorem CKN.Leray.memLp_slab_of_prod {E : Type u_1} [NormedAddCommGroup E] {g : Foundation.Parabolic.Vec3 × ℝ → E} {I : Set ℝ} {p : ENNReal} (h : MeasureTheory.MemLp g p (MeasureTheory.volume.prod (MeasureTheory.volume.restrict I))) : MeasureTheory.MemLp g p (MeasureTheory.volume.restrict (spaceTimeSet Set.univ I))

Square integrability for the product measure is square integrability on the slab.

theorem CKN.Leray.lintegral_slab_spatialGradientSq_le {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) {D : ℝ → ℝ} {T : ℝ} (hD : MeasureTheory.IntegrableOn D (Set.Ioc 0 T) MeasureTheory.volume) (hD0 : ∀ (s : ℝ), 0 ≤ D s) (hle : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 T), ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u (forcedMollifiedGrad u) (x, s)) ≤ ENNReal.ofReal (D s)) : ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (spatialGradientSq u (forcedMollifiedGrad u) z) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) ≤ ENNReal.ofReal (∫ (s : ℝ) in Set.Ioc 0 T, D s)

Tonelli's bound for the dissipation on a slab by the integrated slice bounds.

theorem CKN.Leray.memLp_forcedMollifiedGrad_prod {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) {μ : MeasureTheory.Measure (Foundation.Parabolic.Vec3 × ℝ)} (hfin : ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (spatialGradientSq u (forcedMollifiedGrad u) z) ∂μ < ⊤) : MeasureTheory.MemLp (forcedMollifiedGrad u) 2 μ

Finite dissipation on a slab makes the gradient field square integrable there.

theorem CKN.Leray.ae_Ioi_of_forall_Ioc {P : ℝ → Prop} (h : ∀ (n : ℕ), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (↑n + 1)), P s) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), P s

A property holding almost everywhere on every bounded time interval holds almost everywhere on positive times.

theorem CKN.Leray.eLpNorm_realVectorL2Representative_le (W : ↥RealVectorL2) : MeasureTheory.eLpNorm (realVectorL2Representative W) 2 MeasureTheory.volume ≤ ENNReal.ofReal ‖W‖

The coordinate representative of a real L² field has L² norm at most the norm of the field.

theorem CKN.Leray.memLp_curveRep_prod {U : ℝ → ↥RealVectorL2} (hUc : Continuous U) {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hu : MeasureTheory.StronglyMeasurable u) (hrep : ∀ (s : ℝ), (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U s)) (T : ℝ) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

A jointly measurable representative of a continuous curve of real L² fields is square integrable on bounded slabs.

theorem CKN.Leray.inner_realVectorL2OfCoordinateFunction {W : ↥RealVectorL2} {w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hw : w =ᵐ[MeasureTheory.volume] realVectorL2Representative W) (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : inner ℝ W (realVectorL2OfCoordinateFunction g hg) = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, g x i * w x i

The pairing of a real L² field with a transferred coordinate field is the integral of the pointwise dot product of the representatives.

theorem CKN.Leray.forcedForce_work_eq {U : ℝ → ↥RealVectorL2} (hUc : Continuous U) {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hu : MeasureTheory.StronglyMeasurable u) (hrep : ∀ (s : ℝ), (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U s)) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) {t : ℝ} (ht : 0 < t) : ∫ (s : ℝ) in Set.Ioc 0 t, inner ℝ (U s) (forcedForceSlice (forcedForceMod f hf) s) = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ i : Fin 3, f z i * u z i

The work of the force along the solution curve is the space-time integral of the force against the velocity.