The public statement CIV.Main.interiorAnalyticity

This module proves the statement CIV.interiorAnalyticity: a classical solution of eq:nse:forced on B(R) × (t₁, t₂) with a locally uniformly spatially analytic force is locally uniformly spatially analytic (thm:analytic:interior). The proof is CIV.kahane_interiorAnalyticity: on nested regions inside each compactly contained cylinder, the weighted derivatives of the velocity and the pressure are bounded by a factorial majorant, by induction on the order, through interior gradient bounds for the heat operator and the Laplacian.

theorem CIV.Main.interiorAnalyticity (R t₁ t₂ : ℝ) (hR : 0 < R) (ht : t₁ < t₂) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo t₁ t₂))) (hf : LocallyUniformlyAnalyticOn f R t₁ t₂) : LocallyUniformlyAnalyticOn u R t₁ t₂

The public statement of interior analyticity (thm:analytic:interior).