The slice properties (R1) of the pointwise regularized velocity #
Every nonnegative-time slice of the pointwise velocity represents the global
regularized mild curve, so the velocity inherits the continuity of the curve
in L², the initial trace J_ε a, and weak solenoidality from the coordinate
field of the curve (thm:regularised (R1)).
theorem
CKN.Leray.regR12_isWeakDivFreeL2_congr
{f g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(hfg : f =ᵐ[MeasureTheory.volume] g)
(hf : IsWeakDivFreeL2 f)
:
Weak solenoidality in L² depends only on the almost-everywhere class.
theorem
CKN.Leray.regR12_realVectorL2OfCoordinateFunction_congr
{f g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
(hfg : f =ᵐ[MeasureTheory.volume] g)
:
The real L² field of a coordinate function depends only on its
almost-everywhere class.
theorem
CKN.Leray.regR12Velocity_R1
(ρ : 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))
:
have u := regR12Velocity ρ ε hε a ha;
∃ (hSlice :
∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume),
(Continuous fun (t : ↑(Set.Ici 0)) =>
realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) ∧ (fun (x : Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume] regUniformMollifiedInitial ρ ε hε a ∧ ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)
thm:regularised (R1) for the pointwise regularized velocity.