Taylor derivative series: transport, limits, and gluing

For HasFTaylorSeriesUpTo n f q, if f takes values in a closed subspace, then the Taylor coefficients q x m take values there at every order m ≤ n. The proof uses the closed-subspace derivative criterion at each successive order.

A linear isometry lifts a Taylor derivative series when its coefficients lie in the isometry’s range; this lifting does not require the range to be closed.

Over a real or complex normed field, locally uniform limits of the coefficients of Taylor derivative series are again Taylor derivative series, provided the underlying functions converge pointwise. This is the derivative-compatibility step in completeness of smooth function spaces. The limit argument uses Mathlib's hasFDerivAt_of_tendstoLocallyUniformlyOn.

Taylor series with matching coefficients glue across two closed sets on their union. For a closed cover of the whole space this gives a global piecewise Cᵏ criterion. Finite sums and constant scalar multiples carry the corresponding coefficientwise series.

theorem HasFTaylorSeriesUpTo.apply_mem_of_range_subset {𝕜 : Type u_1} {D : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup D] [NormedSpace 𝕜 D] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : D → F} {q : D → FormalMultilinearSeries 𝕜 D F} {S : Submodule 𝕜 F} (hq : HasFTaylorSeriesUpTo n f q) (hS : IsClosed ↑S) (hf : Set.range f ⊆ ↑S) (m : ℕ) (hm : ↑m ≤ n) (x : D) (v : Fin m → D) : (q x m) v ∈ S

For a Taylor derivative series up to order n of a function valued in a closed subspace, the coefficients of every order m ≤ n take values in that subspace.

theorem HasFTaylorSeriesUpToOn.of_tendstoLocallyUniformlyOn {𝕜 : Type u_1} {D : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup D] [NormedSpace 𝕜 D] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : D → F} {q : D → FormalMultilinearSeries 𝕜 D F} [IsRCLikeNormedField 𝕜] {s : Set D} (hs : IsOpen s) {ι : Type u_4} {l : Filter ι} [l.NeBot] {fᵢ : ι → D → F} {qᵢ : ι → D → FormalMultilinearSeries 𝕜 D F} (h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (fᵢ i) (qᵢ i) s) (hq : ∀ (m : ℕ), ↑m ≤ n → TendstoLocallyUniformlyOn (fun (i : ι) (x : D) => qᵢ i x m) (fun (x : D) => q x m) l s) (hf : ∀ x ∈ s, Filter.Tendsto (fun (i : ι) => fᵢ i x) l (nhds (f x))) : HasFTaylorSeriesUpToOn n f q s

On an open set, locally uniform limits of Taylor derivative series are Taylor derivative series of the pointwise limit. No completeness of the target is needed once limits are given.

theorem HasFTaylorSeriesUpTo.of_tendstoLocallyUniformly {𝕜 : Type u_1} {D : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup D] [NormedSpace 𝕜 D] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : D → F} {q : D → FormalMultilinearSeries 𝕜 D F} [IsRCLikeNormedField 𝕜] {ι : Type u_4} {l : Filter ι} [l.NeBot] {fᵢ : ι → D → F} {qᵢ : ι → D → FormalMultilinearSeries 𝕜 D F} (h : ∀ (i : ι), HasFTaylorSeriesUpTo n (fᵢ i) (qᵢ i)) (hq : ∀ (m : ℕ), ↑m ≤ n → TendstoLocallyUniformly (fun (i : ι) (x : D) => qᵢ i x m) (fun (x : D) => q x m) l) (hf : ∀ (x : D), Filter.Tendsto (fun (i : ι) => fᵢ i x) l (nhds (f x))) : HasFTaylorSeriesUpTo n f q

Locally uniform limits of Taylor derivative series are Taylor derivative series of the pointwise limit. This is the whole-source specialization of the open-set result.

theorem LinearIsometry.exists_hasFTaylorSeriesUpTo_of_comp {𝕜 : Type u_1} {D : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup D] [NormedSpace 𝕜 D] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (i : E →ₗᵢ[𝕜] F) {f : D → E} {n : WithTop ℕ∞} {q : D → FormalMultilinearSeries 𝕜 D F} (hq : HasFTaylorSeriesUpTo n (⇑i ∘ f) q) (hQ : ∀ (m : ℕ), ↑m ≤ n → ∀ (x : D) (v : Fin m → D), (q x m) v ∈ i.range) : ∃ (p : D → FormalMultilinearSeries 𝕜 D E), HasFTaylorSeriesUpTo n f p

A Taylor derivative series of i ∘ f lifts through the linear isometry i when its coefficients of orders m ≤ n lie in the range of i. No closed-range assumption is needed.

theorem HasFTaylorSeriesUpToOn.union_of_isClosed {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : WithTop ℕ∞} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {s t : Set E} (hfs : HasFTaylorSeriesUpToOn k f p s) (hft : HasFTaylorSeriesUpToOn k f p t) (hs : IsClosed s) (ht : IsClosed t) : HasFTaylorSeriesUpToOn k f p (s ∪ t)

Matching values and one common Taylor series glue across two closed sets at every allowed Taylor order.

theorem HasFTaylorSeriesUpToOn.sum {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : WithTop ℕ∞} {ι : Type u_8} {u : Finset ι} {f : ι → E → F} {p : ι → E → FormalMultilinearSeries 𝕜 E F} {s : Set E} (hf : ∀ i ∈ u, HasFTaylorSeriesUpToOn k (f i) (p i) s) : HasFTaylorSeriesUpToOn k (fun (x : E) => ∑ i ∈ u, f i x) (fun (x : E) (m : ℕ) => ∑ i ∈ u, p i x m) s

A finite sum of functions with Taylor series has the finite sum series on the same set.

theorem HasFTaylorSeriesUpToOn.const_smul {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : WithTop ℕ∞} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {s : Set E} (hf : HasFTaylorSeriesUpToOn k f p s) (c : 𝕜) : HasFTaylorSeriesUpToOn k (fun (x : E) => c • f x) (fun (x : E) (m : ℕ) => c • p x m) s

Constant scalar multiplication scales every term of a within-set Taylor series.

theorem HasFTaylorSeriesUpToOn.contDiff_piecewise {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ∞} {f g : E → F} {p q : E → FormalMultilinearSeries 𝕜 E F} {s t : Set E} [DecidablePred fun (x : E) => x ∈ s] (hf : HasFTaylorSeriesUpToOn (↑k) f p s) (hg : HasFTaylorSeriesUpToOn (↑k) g q t) (hs : IsClosed s) (ht : IsClosed t) (hcover : s ∪ t = Set.univ) (hmatch : ∀ x ∈ s ∩ t, ∀ (m : ℕ), ↑m ≤ k → p x m = q x m) : ContDiff 𝕜 (↑k) (s.piecewise f g)

Piecewise functions on two closed sets covering the space are Cᵏ when all boundary Taylor terms through order k agree.