The public statement CIV.Main.serrinInteriorEstimates

This module proves the statement CIV.serrinInteriorEstimates: on a cylindrical annulus inside the unit cylinder where the velocity is bounded, and with the force bounded in C², the velocity and its spatial derivatives through order two are bounded on every smaller annulus, uniformly up to the blow-up time. The proof is CIV.serrin_interior_estimates_of_suitable: the weak solution is classical on the open cylinder, the vorticity equation in divergence form is estimated level by level through its cut-off heat representation and a distance-weighted absorption, and the velocity derivatives are recovered from the vorticity by the Newtonian potential. The energy class is not used.

theorem CIV.Main.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

The public statement of Serrin's interior estimates: bounds for the velocity and its spatial derivatives through order two on a smaller annular cylinder, uniformly up to the blow-up time.