Reg Tails Time Energy Contract #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.regTails_contract_timeGradientBounds
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(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)
(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)
:
have Dplus := regTailsPositiveGradientExtension D;
have B := (MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume).toReal;
have G := fun (t : ℝ) =>
√(∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u Dplus (x, t))).toReal;
(∀ (T : ℝ),
0 < T →
MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T)) ∧ ∫ (t : ℝ) in Set.Ioo 0 T, G t ^ 2 ≤ B ^ 2 / 2 ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u Dplus (x, t)) ≠ ⊤) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => √(spatialGradientSq u D (x, t))) 2
MeasureTheory.volume).toReal = G t
The energy identity gives the time-integrated gradient profile and the
almost every slice identification needed in the flux estimates of
lem:reg-tails.