The forced time modulus

lem:forced-equicontinuity: for a smooth compactly supported spatial test field w, the pairings t ↦ ∫ u_ε(t)·w of the forced regularized solutions have a common Hölder modulus on [0,T], independent of ε. The increment of a pairing between two times is the space-time integral of the momentum flux with the pressure term (the weak momentum identity eq:reg-momentum-forced tested with η(t) w(x)), and Hölder's inequality with the uniform energy, dissipation, L³ and L^{5/3} quadratic-pressure bounds of lem:forced-energy-bounds and the force-pressure bound of lem:force-pressure bounds it by a constant times |t - s|^{2/5}.

theorem CKN.Leray.forcedLerayLimit_time_modulus_uniform (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (hmom : ∀ (ε : ℝ) (hε : 0 < ε), ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε) z j * forcedRegVelocity ρ a ha f hf ε z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, forcedRegGradient ρ a ha f hf ε z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - forcedRegPressure ρ a ha f hf ε z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (T : ℝ) (hT : 0 < T) {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3), ContDiff ℝ (↑⊤) (wc i)) → (∀ (i : Fin 3), tsupport (wc i) ⊆ K) → ∀ (M0 M1 : ℝ), 0 ≤ M0 → 0 ≤ M1 → (∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), |wc i x| ≤ M0) → (∀ (i j : Fin 3) (x : Foundation.Parabolic.Vec3), |spatialDeriv (wc i) j x| ≤ M1) → ∀ (ε : ℝ), 0 < ε → ∀ s ∈ Set.Icc 0 T, ∀ t ∈ Set.Icc 0 T, |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε (x, t) i * wc i x) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε (x, s) i * wc i x| ≤ C * (M0 + M1) * |t - s| ^ (2 / 5)

lem:forced-equicontinuity with a constant independent of the test field: given the weak momentum identity eq:reg-momentum-forced of the forced regularized solutions, there is C, depending only on T, K, the datum and the force, such that for every smooth test field w supported in K with |w| ≤ M₀ and |∂_j w_i| ≤ M₁ the pairings t ↦ ∫ u_ε(t)·w satisfy |∫ (u_ε(t) - u_ε(s))·w| ≤ C (M₀ + M₁) |t - s|^{2/5} on [0,T], for every ε.

theorem CKN.Leray.forcedLerayLimit_time_modulus (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (hmom : ∀ (ε : ℝ) (hε : 0 < ε), ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε) z j * forcedRegVelocity ρ a ha f hf ε z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, forcedRegGradient ρ a ha f hf ε z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - forcedRegPressure ρ a ha f hf ε z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (T : ℝ) (hT : 0 < T) {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) {wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (wc i)) (hwK : ∀ (i : Fin 3), tsupport (wc i) ⊆ K) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε : ℝ), 0 < ε → ∀ s ∈ Set.Icc 0 T, ∀ t ∈ Set.Icc 0 T, |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε (x, t) i * wc i x) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε (x, s) i * wc i x| ≤ B * |t - s| ^ (2 / 5)

lem:forced-equicontinuity: given the weak momentum identity eq:reg-momentum-forced of the forced regularized solutions, for every smooth test field w supported in a compact set K the pairings t ↦ ∫ u_ε(t)·w have a common modulus B |t - s|^{2/5} on [0,T], with B independent of ε.

theorem CKN.Leray.forcedLerayLimit_compactness_modulus (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (hmom : ∀ (ε : ℝ) (hε : 0 < ε), ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, forcedRegVelocity ρ a ha f hf ε z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε) z j * forcedRegVelocity ρ a ha f hf ε z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, forcedRegGradient ρ a ha f hf ε z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - forcedRegPressure ρ a ha f hf ε z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n) (T : ℝ) (hT : 0 < T) (C : Set Foundation.Parabolic.Vec3) : IsCompact C → C ⊆ Set.univ → ∀ (a' b : ℝ), Set.Icc a' b ⊆ Set.Ioo 0 T → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3), ContDiff ℝ (↑⊤) w → HasCompactSupport w → tsupport w ⊆ C → ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), s ∈ Set.Icc a' b → t ∈ Set.Icc a' b → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf (εseq n) (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf (εseq n) (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ

The time modulus of lem:forced-equicontinuity in the form of the time-pairing hypothesis of lem:compactness, for the forced regularized solutions along any sequence of positive regularization parameters, on the time interval (0,T) and for test fields with values in L2Vec3.