A uniform time modulus for regularized pairings

For a smooth, compactly supported, divergence-free test w, the pairing t ↦ ∫ u_ε(x,t) · w(x) dx of a regularized solution of thm:regularised is Lipschitz on [0,∞) with a constant depending only on w and on the energy bound. This is the solenoidal case of lem:reg-equicontinuity: the pressure term vanishes because w is divergence-free.

theorem CKN.Leray.lerayHopfLimit_slice_continuous {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : ContinuousOn F (spaceTimeSet Set.univ (Set.Ioi 0))) {t : ℝ} (ht : 0 < t) : Continuous fun (x : Foundation.Parabolic.Vec3) => F (x, t)

A field continuous on positive times is continuous on each positive time slice.

theorem CKN.Leray.lerayHopfLimit_inner_realVectorL2 (a b : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (hb : MeasureTheory.MemLp b 2 MeasureTheory.volume) : inner ℝ (realVectorL2OfCoordinateFunction a ha) (realVectorL2OfCoordinateFunction b hb) = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, a x i * b x i

The Hilbert-space pairing of two coordinate L² fields is their coordinate dot-product integral.

theorem CKN.Leray.lerayHopfLimit_slice_differentiable (F : Foundation.Parabolic.ParabolicPoint → ℝ) (hC1 : ContDiffOn ℝ 1 F (spaceTimeSet Set.univ (Set.Ioi 0))) (x : Foundation.Parabolic.Vec3) {t : ℝ} (ht : 0 < t) : DifferentiableAt ℝ (fun (s : ℝ) => F (x, s)) t ∧ DifferentiableAt ℝ (fun (y : Foundation.Parabolic.Vec3) => F (y, t)) x

Joint continuous differentiability on positive times gives differentiability along time and along space at every positive-time point.

theorem CKN.Leray.lerayHopfLimit_regPairing_hasDerivAt (U : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (w : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hwc : ∀ (i : Fin 3), HasCompactSupport (w i)) (hUc : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => U z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDtc : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hC1 : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => U z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDtBound : ∀ (δ T : ℝ), 0 < δ → δ < T → ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), ∀ (i : Fin 3), |timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) z| ≤ C) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, s) i * w i x) (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) (x, t) * w i x) t

The time derivative of the pairing of a regularized velocity with a smooth compactly supported test, at a positive time.

theorem CKN.Leray.lerayHopfLimit_regPairing_lipschitz (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (U : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hSliceMem : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => U (x, t)) 2 MeasureTheory.volume) (hSliceCont : Continuous fun (t : ↑(Set.Ici 0)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => U (x, ↑t)) ⋯) (hSliceDiv : ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => U (x, t)) (hUc : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => U z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDc : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) j z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDDc : ∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => U x i) j y) k z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDtc : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hpc : ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0))) (hDpc : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hC1 : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => U z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) j (x, z.2)) z.1) (hpdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) (hDtBound : ∀ (δ T : ℝ), 0 < δ → δ < T → ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), ∀ (i : Fin 3), |timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) z| ≤ C) (hPDE : ∀ (z : Foundation.Parabolic.ParabolicPoint), 0 < z.2 → ∀ (i : Fin 3), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) z - ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => U x i) j y) j z + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε U z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U y i) j z + spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z = 0) (B : ℝ) (hB : ∀ (t : ℝ), 0 ≤ t → (MeasureTheory.eLpNorm (regUniformVelocitySlice U t) 2 MeasureTheory.volume).toReal ≤ B) (w : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hwc : ∀ (i : Fin 3), HasCompactSupport (w i)) (hdivw : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialDeriv (w i) i x = 0) (K : ℝ) (hK : ∀ (f J : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (f i) 2 MeasureTheory.volume) → (∀ (j : Fin 3), MeasureTheory.MemLp (J j) 2 MeasureTheory.volume) → (∀ (i : Fin 3), ∫ (x : Foundation.Parabolic.Vec3), f i x ^ 2 ≤ B ^ 2) → (∀ (j : Fin 3), ∫ (x : Foundation.Parabolic.Vec3), J j x ^ 2 ≤ B ^ 2) → |∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (f i x * spatialDeriv (spatialDeriv (w i) j) j x + f i x * J j x * spatialDeriv (w i) j x)| ≤ K) (s t : ℝ) : 0 ≤ s → 0 ≤ t → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * w i x) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, s) i * w i x| ≤ K * |t - s|

The solenoidal pairing of a regularized solution is Lipschitz in time on [0,∞), with the constant of lerayHopfLimit_pairing_rhs_bound.