Classical spatial regularity of the regularized velocity #
When the global regularized mild curve lifts continuously to the Bessel
potential space of order four on every interval [0,T], the pointwise
velocity of thm:regularised, its first and its second spatial partial
derivatives are continuous on ℝ³ × (0,∞), and the velocity slices and their
first partial derivatives are differentiable.
theorem
CKN.Leray.regR12_spatialPartial_congr_slice
{F F' : Foundation.Parabolic.ParabolicPoint → ℝ}
(z : Foundation.Parabolic.ParabolicPoint)
(h : ∀ (x : Foundation.Parabolic.Vec3), F (x, z.2) = F' (x, z.2))
(j : Fin 3)
:
A spatial partial derivative depends only on the time slice.
theorem
CKN.Leray.regR12_continuousOn_of_local_models
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
(h :
∀ (T : ℝ),
0 < T →
∃ (F' : Foundation.Parabolic.Vec3 × ℝ → ℝ),
Continuous F' ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ∈ Set.Ioo 0 T → F (z.1, z.2) = F' z)
:
ContinuousOn F (spaceTimeSet Set.univ (Set.Ioi 0))
A field that agrees on every slab ℝ³ × (0,T) with a continuous field is
continuous on ℝ³ × (0,∞) for the parabolic topology.
theorem
CKN.Leray.regR12_first_norm_le
(j : Fin 3)
(ξ : Foundation.Parabolic.L2Vec3)
:
‖(fun (ξ : Foundation.Parabolic.L2Vec3) => regR12CoordSymbol j ξ * (fun (x : Foundation.Parabolic.L2Vec3) => 1) ξ) ξ‖ ≤ 2 * Real.pi * (1 + ‖ξ‖ ^ 2)
theorem
CKN.Leray.regR12_second_norm_le
(j k : Fin 3)
(ξ : Foundation.Parabolic.L2Vec3)
:
‖(fun (ξ : Foundation.Parabolic.L2Vec3) =>
regR12CoordSymbol k ξ * (fun (ξ : Foundation.Parabolic.L2Vec3) =>
regR12CoordSymbol j ξ * (fun (x : Foundation.Parabolic.L2Vec3) => 1) ξ)
ξ)
ξ‖ ≤ (2 * Real.pi) ^ 2 * (1 + ‖ξ‖ ^ 2)
theorem
CKN.Leray.regR12Velocity_D_eq_model
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(T : ℝ)
(hT : 0 ≤ T)
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2))
(hv :
∀ (t : ↑(RegularizedMildTimeInterval T)),
(regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z.2 ∈ Set.Icc 0 T)
(i j : Fin 3)
:
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha y i) j z = regR12SpaceTimeField (regR12CoordCLM i)
(fun (ξ : Foundation.Parabolic.L2Vec3) => regR12CoordSymbol j ξ * (fun (x : Foundation.Parabolic.L2Vec3) => 1) ξ)
(regR12LiftFreq T hT v) z
On [0,T], the first spatial partial derivatives of the velocity are the
space-time fields of the lift with the multiplier 2πi ξ_j.
theorem
CKN.Leray.regR12Velocity_DD_eq_model
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(T : ℝ)
(hT : 0 ≤ T)
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2))
(hv :
∀ (t : ↑(RegularizedMildTimeInterval T)),
(regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z.2 ∈ Set.Icc 0 T)
(i j k : Fin 3)
:
spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha x i) j y)
k z = regR12SpaceTimeField (regR12CoordCLM i)
(fun (ξ : Foundation.Parabolic.L2Vec3) =>
regR12CoordSymbol k ξ * (fun (ξ : Foundation.Parabolic.L2Vec3) =>
regR12CoordSymbol j ξ * (fun (x : Foundation.Parabolic.L2Vec3) => 1) ξ)
ξ)
(regR12LiftFreq T hT v) z
On [0,T], the second spatial partial derivatives of the velocity are
the space-time fields of the lift with the multiplier (2πi)² ξ_j ξ_k.
theorem
CKN.Leray.regR12Velocity_slices_differentiableAt
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(T : ℝ)
(hT : 0 ≤ T)
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2))
(hv :
∀ (t : ↑(RegularizedMildTimeInterval T)),
(regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z.2 ∈ Set.Icc 0 T)
(i j : Fin 3)
:
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => regR12Velocity ρ ε hε a ha (x, z.2) i) z.1 ∧ DifferentiableAt ℝ
(fun (x : Foundation.Parabolic.Vec3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha y i) j (x, z.2))
z.1
On [0,T], the velocity slices and their first partial derivatives are
differentiable.
theorem
CKN.Leray.regR12Velocity_slice_ae_eq_curve
(ρ : 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_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(t : ℝ)
(ht : 0 ≤ t)
:
(fun (x : Foundation.Parabolic.Vec3) => regR12Velocity ρ ε hε a ha (x, t)) =ᵐ[MeasureTheory.volume]
realVectorL2Representative (regR12Curve ρ ε hε a ha t)
Every nonnegative-time slice of the velocity represents the global curve.
theorem
CKN.Leray.regR12Velocity_continuousOn
(ρ : 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_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(i : Fin 3)
:
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha z i)
(spaceTimeSet Set.univ (Set.Ioi 0))
The velocity is continuous on ℝ³ × (0,∞).
theorem
CKN.Leray.regR12Velocity_D_continuousOn
(ρ : 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_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(i j : Fin 3)
:
ContinuousOn
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha y i) j z)
(spaceTimeSet Set.univ (Set.Ioi 0))
The first spatial partial derivatives of the velocity are continuous on
ℝ³ × (0,∞).
theorem
CKN.Leray.regR12Velocity_DD_continuousOn
(ρ : 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_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(i j k : Fin 3)
:
ContinuousOn
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha x i) j y)
k z)
(spaceTimeSet Set.univ (Set.Ioi 0))
The second spatial partial derivatives of the velocity are continuous on
ℝ³ × (0,∞).
theorem
CKN.Leray.regR12Velocity_differentiableAt
(ρ : 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_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t))
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ spaceTimeSet Set.univ (Set.Ioi 0))
(i j : Fin 3)
:
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => regR12Velocity ρ ε hε a ha (x, z.2) i) z.1 ∧ DifferentiableAt ℝ
(fun (x : Foundation.Parabolic.Vec3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha y i) j (x, z.2))
z.1
The velocity slices and their first partial derivatives are differentiable at positive times.