The two spatial-analyticity predicates

eq:interior:force:analytic and eq:analytic:interior:force state the same locally uniform spatial analyticity bound, once for the force on the unit cylinder and once for a general field on B(R) × (t₁, t₂). This module records the identity of the two readings at the unit cylinder, and the restriction step that turns a single analyticity bound on a closed time interval into the locally uniform statement, by monotonicity in the ball and in the interval.

The companion restriction on the other side of lem:analytic:slice is IsClassicalSolutionOn.mono: being a classical solution is inherited by every subset of the space-time set on which it holds, so the hypothesis may be read on the smaller cylinder the analyticity statement is applied to.

theorem CIV.forceSpatiallyAnalytic_iff_locallyUniformlyAnalyticOn (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : ForceSpatiallyAnalytic f ↔ LocallyUniformlyAnalyticOn f 1 (-1) 0

Spatial analyticity of the force on the unit cylinder, eq:interior:force:analytic, is the locally uniform analyticity of eq:analytic:interior:force at R = 1 on the time interval (-1, 0): the two definitions unfold to the same proposition.

theorem CIV.locallyUniformlyAnalyticOn_of_analyticBoundOn {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' t₁ t₂ M a : ℝ} (h : AnalyticBoundOn g R' (Set.Icc t₁ t₂) M a) (ha : 0 < a) : LocallyUniformlyAnalyticOn g R' t₁ t₂

One analyticity bound on B(R') × [t₁, t₂] already gives the locally uniform statement on B(R') × (t₁, t₂): every smaller ball and every compactly contained closed time interval inherit the same constants M, a. This is the restriction step owed by lem:analytic:slice away from R = 1.

theorem CIV.IsClassicalSolutionOn.mono {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {S T : Set CKN.Foundation.Parabolic.ParabolicPoint} (h : IsClassicalSolutionOn u p f S) (hTS : T ⊆ S) : IsClassicalSolutionOn u p f T

Being a classical solution of eq:nse:forced is inherited by subsets: the smoothness of the three fields restricts by ContDiffOn.mono, and the momentum and divergence equations are pointwise conditions, so they hold at every point of the smaller set.