Interior Analyticity

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

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

Theorem 2.1 (thm:analytic:interior, Kahane 1969): interior spatial analyticity.