Transfer of the analyticity bound along agreement on the unit cylinder

AnalyticBoundOn and ForceSpatiallyAnalytic read only spatial derivatives at points of B(1) × (-1, 0), and each such derivative is determined by the field on a spatial neighbourhood inside that cylinder. So the analyticity bound eq:analytic:interior:force, and with it eq:interior:force:analytic, transfers between two fields that merely agree on the unit cylinder.

The consequence used by cor:interior:nonanalytic is the last theorem below: a force that vanishes identically on the unit cylinder agrees there with the zero field, which satisfies eq:interior:force:analytic by forceSpatiallyAnalytic_const. Contrapositively, a force that violates eq:interior:force:analytic is somewhere nonzero on the unit cylinder, which is the corollary's step from its first conclusion to its second, f ≢ 0.

theorem CIV.multiPartial_congr_of_eqOn_unitCylinder {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (heq : Set.EqOn g h unitCylinder) (α : Fin 3 → ℕ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : multiPartial g α z = multiPartial h α z

Two scalar fields agreeing on the unit cylinder have equal multi-index spatial partial derivatives at every point of the unit cylinder: each of the three iterated directional derivatives is taken at fixed time inside the open ball B(1).

theorem CIV.analyticBoundOn_congr_of_eqOn_unitCylinder {g h : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' : ℝ} {J : Set ℝ} {M a : ℝ} (hR' : R' ≤ 1) (hJ : J ⊆ Set.Ioo (-1) 0) (heq : Set.EqOn g h unitCylinder) (hb : AnalyticBoundOn h R' J M a) : AnalyticBoundOn g R' J M a

The analyticity bound eq:analytic:interior:force transfers between two vector fields that agree on the unit cylinder, on every cylinder B(R') × J the unit one contains. Only agreement on the unit cylinder is assumed, not at every point of space-time.

theorem CIV.forceSpatiallyAnalytic_congr_of_eqOn_unitCylinder {f g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (heq : Set.EqOn f g unitCylinder) (hg : ForceSpatiallyAnalytic g) : ForceSpatiallyAnalytic f

Spatial analyticity of the force, eq:interior:force:analytic, transfers between two forces that agree on the unit cylinder: the predicate is read on subcylinders B(R) × [t₁, t₂] with R < 1 and -1 < t₁, t₂ < 0, all of which sit inside the unit cylinder.

theorem CIV.forceSpatiallyAnalytic_of_eqOn_unitCylinder_zero {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (heq : ∀ z ∈ unitCylinder, f z = 0) : ForceSpatiallyAnalytic f

A force that vanishes identically on the unit cylinder satisfies eq:interior:force:analytic: it agrees there with the zero field, for which every derivative of positive order vanishes.

theorem CIV.exists_mem_unitCylinder_ne_zero_of_not_forceSpatiallyAnalytic {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ¬ForceSpatiallyAnalytic f) : ∃ z ∈ unitCylinder, f z ≠ 0

The step of cor:interior:nonanalytic from its first conclusion to its second: a force violating eq:interior:force:analytic cannot vanish identically on the unit cylinder, so f ≢ 0 there.