From multilinear map norm to sum over basis evaluations

theorem CIV.norm_le_sum_abs_apply_basis {n : ℕ} (A : CKN.Foundation.Parabolic.Vec3 [×n]→L[ℝ] ℝ) : ‖A‖ ≤ ∑ v : Fin n → Fin 3, |A fun (i : Fin n) => CKN.basisVec (v i)|

The operator norm of a continuous multilinear map on Vec3 is bounded by the sum of the absolute values of its evaluations on the coordinate-basis tuples. This is the elementary estimate that turns the factorial bound on multiPartial, eq:analytic:interior:velocity, into a factorial bound on the operator norm of iteratedFDeriv, as used in thm:analytic:interior.

Factorial bounds on iterated derivatives from the multi-index bound

theorem CIV.foldr_axisDeriv_replicate (j : Fin 3) (k : ℕ) (G : CKN.Foundation.Parabolic.Vec3 → ℝ) : List.foldr axisDeriv G (List.replicate k j) = (axisDeriv j)^[k] G

Folding axisDeriv j over a list of k copies of the same direction j agrees with iterating axisDeriv j itself k times.

theorem CIV.norm_iteratedFDeriv_le_of_analyticBoundOn {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' M a t : ℝ} {J : Set ℝ} (ht : t ∈ J) (ha : 0 < a) (i : Fin 3) (hsmooth : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 R')) (hb : AnalyticBoundOn g R' J M a) (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 R' → ‖iteratedFDeriv ℝ n (fun (y : CKN.Foundation.Parabolic.Vec3) => g (y, t) i) x‖ ≤ M * (3 / a) ^ n * ↑n.factorial

Factorial bound on the iterated Fréchet derivative of a slice component. The multi-index bound AnalyticBoundOn, eq:analytic:interior:force, controls every iterated axisDeriv composition; summing over the 3^n coordinate-basis tuples of norm_le_sum_abs_apply_basis turns this into the factorial bound on iteratedFDeriv that analyticOnNhd_vec3Ball_of_iteratedFDeriv_bound consumes for thm:analytic:interior.

Analyticity of a time slice from locally uniform bounds

theorem CIV.analyticOnNhd_slice_of_locallyUniformlyAnalyticOn {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R t₁ t₂ : ℝ} (hsmooth : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo t₁ t₂))) (hg : LocallyUniformlyAnalyticOn g R t₁ t₂) (t : ℝ) : t ∈ Set.Ioo t₁ t₂ → ∀ (i : Fin 3), AnalyticOnNhd ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 R)

Spatial analyticity of a time slice from local uniform bounds. This combines the factorial bound norm_iteratedFDeriv_le_of_analyticBoundOn with the analyticity criterion analyticOnNhd_vec3Ball_of_iteratedFDeriv_bound to conclude thm:analytic:interior: every Cartesian component of a locally uniformly analytic field, at a fixed time in (t₁, t₂), is real analytic on the spatial ball B(R).