Real analyticity from factorial bounds on the derivatives

The quantitative analyticity of eq:analytic:slice:force and eq:analytic:interior:velocity is a family of bounds ‖∂^α u‖ ≤ M a^{-|α|} |α|! on the derivatives. The identity theorem, on the other hand, is stated for Mathlib's AnalyticOnNhd. This file supplies the missing implication: a smooth function whose iterated derivatives obey ‖D^n f‖ ≤ C K^n n! on a ball is real analytic there.

The proof is the classical one. Taylor's formula with the integral remainder, map_add_eq_sum_add_integral_iteratedFDeriv, writes the difference between f (x + y) and the n-th Taylor polynomial as an integral over the segment [x, x + y]; the factorial bound makes that remainder at most C (n + 1) (K‖y‖)^{n + 1}, which tends to 0 as soon as K‖y‖ < 1. The same bound makes the Taylor series absolutely convergent on that ball, so its sum is f (x + y), which is a power series expansion of f at x.

Mathlib has the converse implication (AnalyticAt gives Cauchy estimates on the iterated derivatives) but not this direction, so the criterion is proved here from Taylor's formula.

The last section restricts a space-time field to one time slice, which is the form in which the criterion is applied to the velocity.

theorem CIV.norm_sub_taylorSum_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {x y : E} {C K r : ℝ} (n : ℕ) (hy : ‖y‖ < r) (hf : ContDiffOn ℝ (↑⊤) f (Metric.ball x r)) (hbound : ∀ (m : ℕ), ∀ z ∈ Metric.ball x r, ‖iteratedFDeriv ℝ m f z‖ ≤ C * K ^ m * ↑m.factorial) : ‖f (x + y) - ∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ • (iteratedFDeriv ℝ k f x) fun (x : Fin k) => y‖ ≤ C * ↑(n + 1) * (K * ‖y‖) ^ (n + 1)

The Taylor remainder of order n at x in the direction y, estimated from factorial bounds on the iterated derivatives along the segment from x to x + y.

theorem CIV.analyticAt_of_norm_iteratedFDeriv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {x : E} {C K r : ℝ} (hr : 0 < r) (hK : 0 < K) (hf : ContDiffOn ℝ (↑⊤) f (Metric.ball x r)) (hbound : ∀ (n : ℕ), ∀ z ∈ Metric.ball x r, ‖iteratedFDeriv ℝ n f z‖ ≤ C * K ^ n * ↑n.factorial) : AnalyticAt ℝ f x

Real analyticity from factorial bounds on the iterated derivatives. A smooth function whose iterated derivatives satisfy ‖D^n f‖ ≤ C K^n n! on a ball around x is real analytic at x: its Taylor series at x converges to it on the ball of radius min r K⁻¹.

theorem CIV.analyticOnNhd_of_norm_iteratedFDeriv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {s : Set E} {C K : ℝ} (hs : IsOpen s) (hK : 0 < K) (hf : ContDiffOn ℝ (↑⊤) f s) (hbound : ∀ (n : ℕ), ∀ z ∈ s, ‖iteratedFDeriv ℝ n f z‖ ≤ C * K ^ n * ↑n.factorial) : AnalyticOnNhd ℝ f s

The same criterion on an open set, with one pair of constants for the whole set.

theorem CIV.analyticOnNhd_vec3Ball_of_iteratedFDeriv_bound {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {G : CKN.Foundation.Parabolic.Vec3 → F} {R : ℝ} (hG : ContDiffOn ℝ (↑⊤) G (CKN.Foundation.Parabolic.vec3Ball 0 R)) (hbound : ∀ R' < R, ∃ (C : ℝ) (K : ℝ), 0 < K ∧ ∀ (n : ℕ), ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 R', ‖iteratedFDeriv ℝ n G x‖ ≤ C * K ^ n * ↑n.factorial) : AnalyticOnNhd ℝ G (CKN.Foundation.Parabolic.vec3Ball 0 R)

Analyticity on a ball from locally uniform factorial bounds. This is the shape in which the quantitative analyticity eq:analytic:interior:velocity is available: on every ball B(R') compactly contained in B(R) the iterated derivatives obey a factorial bound, with constants allowed to degenerate as R' ↑ R. The conclusion is analyticity on all of B(R).

theorem CIV.contDiffOn_slice_component {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R t t₁ t₂ : ℝ} (ht : t ∈ Set.Ioo t₁ t₂) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo t₁ t₂))) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 R)

One component of one time slice of a field that is smooth on a space-time cylinder is smooth on the spatial ball.