The classical time derivative of the regularized velocity #
The time-derivative theorem for velocities that satisfy the regularized
equation weakly applies to the pointwise regularized velocity and the
canonical pressure of thm:regularised. Its hypotheses are supplied by:
- the Bessel lift of the global regularized mild curve;
- the pressure regularity;
- the spatial regularity of the velocity.
theorem
CKN.Leray.regR12_hasDerivAt_of_inputs
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(hPath :
∀ (T : ℝ),
0 ≤ T →
∃ (v :
C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)),
∀ (t : ↑(RegularizedMildTimeInterval T)),
(regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_hasDerivAt_of_inputs._proof_1) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(hPress :
have p := forcedQuadPressure ρ ε hε (regR12Curve ρ ε hε a ha);
ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (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))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
∃ (C : ℝ),
0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T),
|p z| ≤ C ∧ ∀ (i : Fin 3),
|spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z| ≤ C) ∧ ∀ (δ T : ℝ),
0 < δ →
δ < T →
MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T))) ∧ ∀ (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))))
(hTimeDerivative :
∀ (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ),
(∀ (t : ℝ),
0 ≤ t →
(fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume]
realVectorL2Representative
(regularizedGlobalMildCurve ρ ε hε
(realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) ⋯ t)) →
(∀ (z : Foundation.Parabolic.ParabolicPoint),
0 < z.2 →
p z = forcedQuadPressure ρ ε hε
(regularizedGlobalMildCurve ρ ε hε
(realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) ⋯)
z) →
(∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) →
(∀ (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))) →
(∀ (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))) →
ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) →
(∀ (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))) →
(∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
∀ (i : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => u (x, z.2) i) z.1) →
(∀ 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) →
(∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) →
∀ (z : Foundation.Parabolic.ParabolicPoint),
0 < z.2 →
∀ (i : Fin 3),
HasDerivAt (fun (s : ℝ) => u (z.1, s) i)
(∑ 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)
z.2)
(z : Foundation.Parabolic.ParabolicPoint)
:
0 < z.2 →
∀ (i : Fin 3),
HasDerivAt (fun (s : ℝ) => regR12Velocity ρ ε hε a ha (z.1, s) i)
(regR12TimeRHS ρ ε hε (regR12Velocity ρ ε hε a ha) (forcedQuadPressure ρ ε hε (regR12Curve ρ ε hε a ha)) z i) z.2
The classical time derivative of the regularized velocity, from the time-derivative theorem for velocities satisfying the regularized equation weakly, the Bessel lift and the pressure regularity.