Enstrophy Gronwall

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.deriv_le_of_closure_energy {Y M G W : ℝ → ℝ} {tη Cstar η Cη : ℝ} (hC : 0 ≤ Cstar) (hM : ∀ t ∈ Set.Ioo tη 0, 0 ≤ M t) (hY : ∀ t ∈ Set.Ioo tη 0, 0 ≤ Y t) (hG : ∀ t ∈ Set.Ioo tη 0, G t ≤ η / -t) (hW0 : ∀ t ∈ Set.Ioo tη 0, 0 ≤ W t) (hW : ∀ t ∈ Set.Ioo tη 0, W t ≤ Cη * (-t) ^ (-η)) (henergy : ∀ t ∈ Set.Ioo tη 0, deriv Y t + M t ≤ Cstar * (G t + W t ^ 2 + 1) * (Y t + 1)) (t : ℝ) : t ∈ Set.Ioo tη 0 → deriv Y t ≤ Cstar * (η / -t + Cη ^ 2 * (-t) ^ (-(2 * η)) + 1) * (Y t + 1)

The substitution step that turns the localized energy inequality eq:aniso:closure:energy into the differential inequality closure_gronwall_bound consumes. Dropping the nonnegative dissipation M and inserting the two bounds G ≤ η/(-t) of eq:aniso:G:bound and W ≤ Cη (-t)^{-η} of eq:aniso:closure:w replaces the coefficient Cstar (G + W² + 1) by Cstar (η/(-t) + Cη² (-t)^{-2η} + 1), which is the integrand of the exponential in lem:aniso:closure. The squared swirl bound uses 0 ≤ W, which holds since W is a supremum norm, together with the identity ((-t)^{-η})² = (-t)^{-2η}, valid since -t > 0.

theorem CIV.closure_gronwall_bound {Y : ℝ → ℝ} {tη Cstar η Cη : ℝ} (htη : tη < 0) (hC : 0 ≤ Cstar) (hη : 0 < η ∧ 2 * η < 1) (hCη : 0 ≤ Cη) (hcont : ∀ t ∈ Set.Ico tη 0, ContinuousOn Y (Set.Icc tη t)) (hderiv : ∀ t ∈ Set.Ioo tη 0, HasDerivWithinAt Y (deriv Y t) (Set.Ici t) t) (hY0 : 0 ≤ Y tη) (hineq : ∀ t ∈ Set.Ioo tη 0, deriv Y t ≤ Cstar * (η / -t + Cη ^ 2 * (-t) ^ (-(2 * η)) + 1) * (Y t + 1)) : ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, Y t + 1 ≤ C' * (-t) ^ (-(Cstar * η))

Time-weighted Gronwall bound: if Y satisfies a differential inequality on (tη, 0) with a singular weight (-t)^(-Cstar*η), then Y(t)+1 is bounded by a constant times (-t)^(-Cstar*η). This is the key estimate in the proof of lem:aniso:closure in arXiv:2609.20803.