Spatial tails of regularized Leray solutions

The local energy identity and the uniform global energy bounds control the velocity outside large balls, as in lem:reg-tails.

theorem CKN.Leray.regTails_positiveTimeMeasure_eq_product : regUniformPositiveTimeMeasure = MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioi 0))

The positive-time spacetime measure is the product of spatial volume and one-dimensional volume restricted to positive times.

noncomputable def CKN.Leray.regTailsPositiveGradientExtension (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3

Extending the spatial gradient by zero off positive spacetime preserves measurability, so the global dissipation can be integrated by slices.

Equations

• CKN.Leray.regTailsPositiveGradientExtension D = (CKN.spaceTimeSet Set.univ (Set.Ioi 0)).piecewise D 0

theorem CKN.Leray.regTails_positiveGradientExtension_measurable (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) (spaceTimeSet Set.univ (Set.Ioi 0))) : Measurable (regTailsPositiveGradientExtension D)

theorem CKN.Leray.regTails_scalarTimeProduct_test (q : Foundation.Parabolic.Vec3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (η : ℝ → ℝ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηI : tsupport η ⊆ Set.Ioi 0) : (fun (z : Foundation.Parabolic.Vec3 × ℝ) => q z.1 * η z.2) ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)

A product of compact smooth spatial and positive-time tests is an admissible scalar space-time test.

theorem CKN.Leray.regTails_energy_bounds (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hR5 : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u D t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) (spaceTimeSet Set.univ (Set.Ioi 0))) (hU : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hSpatialC1 : ∀ (t : ℝ), 0 < t → ∀ (i : Fin 3), ContDiff ℝ ↑1 fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) (hDerivative : ∀ (t : ℝ), 0 < t → ∀ (x : Foundation.Parabolic.Vec3) (i j : Fin 3), (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => u (y, t) i) x) (basisVec j) = D (x, t) i j) : (∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 ≤ MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume ^ 2) ∧ 2 * ∫⁻ (z : Foundation.Parabolic.ParabolicPoint), ENNReal.ofReal (spatialGradientSq u D z) ∂regUniformPositiveTimeMeasure ≤ MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume ^ 2 ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∃ (h : Fin 3 → H1Function Set.univ), (∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) ∧ ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = D (x, t) i j

Slice energy, finite total dissipation, and almost every positive-time H¹ slice follow from the R5 identity in lem:reg-tails. The gradient is extended measurably from positive time before applying the global energy estimate.