The time derivative field in (R2)

The classical time derivative of the regularized velocity is the field Δu - (J_ε u · ∇) u - ∇p. From the continuity, strip bounds and slab integrability of the velocity, its spatial derivatives, the pressure gradient and the transport velocity, this field is continuous on ℝ³ × (0,∞), bounded on strips and square integrable on slabs, as required by thm:regularised (R2).

noncomputable def CKN.Leray.regR12TimeRHS (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) : ℝ

The right-hand side Δu_i - (J_ε u · ∇) u_i - ∂_i p.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regR12_timePartial_eq_of_hasDerivAt {g : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {c : ℝ} (h : HasDerivAt (fun (s : ℝ) => g (z.1, s)) c z.2) : timePartial g z = c

The time partial derivative is the derivative along the time line.

theorem CKN.Leray.regR12_mollifiedVelocity_continuousOn_parabolic (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hSlice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hU : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (i : Fin 3) : ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u z i) (spaceTimeSet Set.univ (Set.Ioi 0))

The transport velocity is continuous on ℝ³ × (0,∞) for the parabolic topology.

theorem CKN.Leray.regR12TimeRHS_continuousOn (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hSlice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hU : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hD : ∀ (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))) (hDD : ∀ (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))) (hDp : ∀ (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))) (i : Fin 3) : ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => regR12TimeRHS ρ ε hε u p z i) (spaceTimeSet Set.univ (Set.Ioi 0))

The time derivative field is continuous on ℝ³ × (0,∞).

theorem CKN.Leray.regR12TimeRHS_abs_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hSlice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (C t : ℝ) (ht : 0 < t) (hUb : ∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ C) (hDb : ∀ (x : Foundation.Parabolic.Vec3) (i j : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, t)| ≤ C) (hDDb : ∀ (x : Foundation.Parabolic.Vec3) (i j k : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k (x, t)| ≤ C) (hDpb : ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i (x, t)| ≤ C) (x : Foundation.Parabolic.Vec3) (i : Fin 3) : |regR12TimeRHS ρ ε hε u p (x, t) i| ≤ 3 * C + 3 * ((C * ∫ (y : Foundation.Parabolic.Vec3), |regMollifierKernel ρ ε hε (WithLp.toLp 2 y)|) * C) + C

A strip bound for the time derivative field.

theorem CKN.Leray.regR12TimeRHS_memLp_slab (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (δ T : ℝ) (hSlice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hU : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hD : ∀ (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))) (hδ : 0 < δ) (hDL2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) (hDDL2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) (hDpL2 : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) (CJ : ℝ) (hJ : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioo δ T), ∀ (j : Fin 3), |regUniformMollifiedVelocity ρ ε hε u z j| ≤ CJ) (i : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => regR12TimeRHS ρ ε hε u p z i) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))

Square integrability of the time derivative field on a slab.