Regularity facts about the cutoff enstrophy #
This file exposes, as public reusable facts, the nonnegativity of the cutoff enstrophy Y and
its dissipation M of lem:aniso:closure (currently only proved inline, privately, inside
CIV.energy_inequality_of_mixed_term_bound's own proof) and the continuity/one-sided-derivative
consequences of the differentiation-under-the-integral-sign fact
hasDerivAt_cutoffEnstrophy. These four facts are exactly the hM, hY, hcont, hderiv,
hY0 data that CIV.deriv_le_of_closure_energy and CIV.closure_gronwall_bound need to
run on the concrete quantities Y := cutoffEnstrophy χ u and M := cutoffEnstrophyDissipation χ u.
theorem
CIV.cutoffEnstrophy_nonneg
(χ : CKN.Foundation.Parabolic.Vec3 → ℝ)
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(t : ℝ)
:
theorem
CIV.cutoffEnstrophyDissipation_nonneg
(χ : CKN.Foundation.Parabolic.Vec3 → ℝ)
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(t : ℝ)
:
theorem
CIV.continuousOn_cutoffEnstrophy
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{χ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(hχs : HasCompactSupport χ)
(hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1)
{tη s : ℝ}
(htη : tη ∈ Set.Ioo (-1) 0)
(hs : s ∈ Set.Ico tη 0)
:
ContinuousOn (cutoffEnstrophy χ u) (Set.Icc tη s)
theorem
CIV.hasDerivWithinAt_Ici_cutoffEnstrophy
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{χ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(hχs : HasCompactSupport χ)
(hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1)
{tη t : ℝ}
(htη : tη ∈ Set.Ioo (-1) 0)
(ht : t ∈ Set.Ioo tη 0)
:
HasDerivWithinAt (cutoffEnstrophy χ u) (deriv (cutoffEnstrophy χ u) t) (Set.Ici t) t