Serrin Interior Estimates

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

theorem CIV.serrinInteriorEstimates (q : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (henergy : GlobalEnergyClass u Du p) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hMf : ForceC2Bounded f) (Rm Rp t₀ : ℝ) (hR : 0 ≤ Rm ∧ Rm < Rp ∧ Rp ≤ 1) (ht₀ : t₀ ∈ Set.Ioo (-1) 0) (Mu : ℝ) (hbdd : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) (Rm' Rp' t₀' : ℝ) (hR' : Rm < Rm' ∧ Rm' < Rp' ∧ Rp' < Rp) (ht₀' : t₀ < t₀' ∧ t₀' < 0) : ∃ (K : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm' < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp' → ∀ t ∈ Set.Ioo t₀' 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ K

Serrin's interior estimates, in the form in which the proof of lem:aniso:annulus consumes them (Serrin 1962, Section 4 with m = 1): on a cylindrical annulus {Rm < |x| < Rp} × (t₀, 0) inside Q on which the velocity is bounded, and with the force bounded in C²_x, the velocity and its spatial derivatives through order two are bounded on every smaller annulus {Rm' < |x| < Rp'} × (t₀', 0), uniformly up to the blow-up time.

The bound K is produced after all the data, so no uniformity is asserted: the manuscript's constants "depend only on the subset, on M_f, on sup |u| over the cylindrical annulus, and on ‖∇u‖_{L²(Q)}" (proof of lem:aniso:annulus), and the consumers fix the annulus before every other parameter. The L²(Q) gradient norm and the pressure up to t = 0 come from henergy, not from hsol, whose integrability clauses only see boxes compactly contained in Q (design note R6). The shrinking of the time interval is the manuscript's own t₀ ↦ t₀ + ϱ².

This statement bundles Serrin's printed estimates with the manuscript's argument that they are uniform up to t = 0, because his representation formulas are one-sided in time. The force is the manuscript's own f: the correction of foot:aniso:pressure is not used here ("the derivative estimates ... are written with f itself", footnote foot:aniso:pressure). The proof uses fewer inputs than listed here; see deviation D13 in docs/DEVIATIONS.md.