Base case of the induction on derivative order #
The order 0 and order 1 base case of the induction on derivative order behind
thm:analytic:interior (Kahane 1969): a merely C^∞ field is automatically bounded, together
with its first derivatives, on any closed sub-ball of its domain of smoothness, by the
extreme value theorem on the compact closure CIV.isCompact_closure_vec3Ball. No a priori
bound on u is assumed by CIV.interiorAnalyticity, so this is the only source of a
starting bound for the recursion that produces the full factorial-type estimate
AnalyticBoundOn, eq:analytic:interior:force.
theorem
CIV.exists_bound_of_contDiffOn_zero
{G : CKN.Foundation.Parabolic.Vec3 → ℝ}
{R r : ℝ}
(hr : 0 < r)
(hrR : r < R)
(hG : ContDiffOn ℝ (↑⊤) G (CKN.Foundation.Parabolic.vec3Ball 0 R))
:
∃ (M : ℝ), ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 r, |G x| ≤ M
theorem
CIV.exists_bound_of_contDiffOn_one
{G : CKN.Foundation.Parabolic.Vec3 → ℝ}
{R r : ℝ}
(hr : 0 < r)
(hrR : r < R)
(hG : ContDiffOn ℝ (↑⊤) G (CKN.Foundation.Parabolic.vec3Ball 0 R))
:
theorem
CIV.analyticBoundOn_order_le_one_of_contDiffOn
{g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{R r t : ℝ}
(hr : 0 < r)
(hrR : r < R)
(i : Fin 3)
(hg : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 R))
:
∃ (M : ℝ),
∀ (α : Fin 3 → ℕ),
α 0 + α 1 + α 2 ≤ 1 →
∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 r,
|multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w i) α (x, t)| ≤ M