A constant field trivially satisfies the factorial-type analyticity bound
AnalyticBoundOn / LocallyUniformlyAnalyticOn / ForceSpatiallyAnalytic of
eq:analytic:interior:force at any positive rate a, since every derivative of
positive order vanishes — the base instance the inductive derivative estimates
behind thm:analytic:interior (Kahane 1969) specialize to on a field with no
spatial dependence, such as a zero force.
theorem
CIV.multiPartial_const_eq_zero_of_le
{c : ℝ}
{α : Fin 3 → ℕ}
(hα : 1 ≤ α 0 + α 1 + α 2)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
theorem
CIV.analyticBoundOn_const
{c : CKN.Foundation.Parabolic.Vec3}
{M R' a : ℝ}
(hM : ∀ (i : Fin 3), |c i| ≤ M)
(ha : 0 < a)
{J : Set ℝ}
:
AnalyticBoundOn (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => c) R' J M a
theorem
CIV.locallyUniformlyAnalyticOn_const
{c : CKN.Foundation.Parabolic.Vec3}
{M R t₁ t₂ : ℝ}
(hM : ∀ (i : Fin 3), |c i| ≤ M)
:
LocallyUniformlyAnalyticOn (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => c) R t₁ t₂
theorem
CIV.forceSpatiallyAnalytic_const
{c : CKN.Foundation.Parabolic.Vec3}
{M : ℝ}
(hM : ∀ (i : Fin 3), |c i| ≤ M)
:
ForceSpatiallyAnalytic fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => c