Smoothness of series

We show that series of functions are differentiable, or smooth, when each individual function in the series is and additionally suitable uniform summable bounds are satisfied.

More specifically,

• differentiable_tsum ensures that a series of differentiable functions is differentiable.
• contDiff_tsum ensures that a series of smooth functions is smooth.

We also give versions of these statements which are localized to a set.

Differentiability

theorem summable_of_summable_hasFDerivAt_of_isPreconnected {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ : E} {x : E} (hu : Summable u) (hs : IsOpen s) (h's : IsPreconnected s) (hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun (x : α) => f x x₀) (hx : x ∈ s) : Summable fun (n : α) => f n x

Consider a series of functions ∑' n, f n x on a preconnected open set. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series converges everywhere on the set.

theorem summable_of_summable_hasDerivAt_of_isPreconnected {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {g' : α → 𝕜 → F} {t : Set 𝕜} {y₀ : 𝕜} {y : 𝕜} (hu : Summable u) (ht : IsOpen t) (h't : IsPreconnected t) (hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable fun (x : α) => g x y₀) (hy : y ∈ t) : Summable fun (n : α) => g n y

Consider a series of functions ∑' n, f n x on a preconnected open set. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series converges everywhere on the set.

theorem hasFDerivAt_tsum_of_isPreconnected {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ : E} {x : E} (hu : Summable u) (hs : IsOpen s) (h's : IsPreconnected s) (hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun (n : α) => f n x₀) (hx : x ∈ s) : HasFDerivAt (fun (y : E) => ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Consider a series of functions ∑' n, f n x on a preconnected open set. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable on the set and its derivative is the sum of the derivatives.

theorem hasDerivAt_tsum_of_isPreconnected {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {g' : α → 𝕜 → F} {t : Set 𝕜} {y₀ : 𝕜} {y : 𝕜} (hu : Summable u) (ht : IsOpen t) (h't : IsPreconnected t) (hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable fun (n : α) => g n y₀) (hy : y ∈ t) : HasDerivAt (fun (z : 𝕜) => ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Consider a series of functions ∑' n, f n x on a preconnected open set. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable on the set and its derivative is the sum of the derivatives.

theorem summable_of_summable_hasFDerivAt {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {x₀ : E} (hu : Summable u) (hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) (hf0 : Summable fun (n : α) => f n x₀) (x : E) : Summable fun (n : α) => f n x

Consider a series of functions ∑' n, f n x. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series converges everywhere.

theorem summable_of_summable_hasDerivAt {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {g' : α → 𝕜 → F} {y₀ : 𝕜} (hu : Summable u) (hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) (hg0 : Summable fun (n : α) => g n y₀) (y : 𝕜) : Summable fun (n : α) => g n y

Consider a series of functions ∑' n, f n x. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series converges everywhere.

theorem hasFDerivAt_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {x₀ : E} (hu : Summable u) (hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) (hf0 : Summable fun (n : α) => f n x₀) (x : E) : HasFDerivAt (fun (y : E) => ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Consider a series of functions ∑' n, f n x. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable and its derivative is the sum of the derivatives.

theorem hasDerivAt_tsum {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {g' : α → 𝕜 → F} {y₀ : 𝕜} (hu : Summable u) (hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) (hg0 : Summable fun (n : α) => g n y₀) (y : 𝕜) : HasDerivAt (fun (z : 𝕜) => ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Consider a series of functions ∑' n, f n x. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable and its derivative is the sum of the derivatives.

theorem differentiable_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} (hu : Summable u) (hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) (hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) : Differentiable 𝕜 fun (y : E) => ∑' (n : α), f n y

Consider a series of functions ∑' n, f n x. If all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable. Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise convergence then the series is zero everywhere so the result still holds.

theorem differentiable_tsum' {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {g' : α → 𝕜 → F} (hu : Summable u) (hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) (hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) : Differentiable 𝕜 fun (z : 𝕜) => ∑' (n : α), g n z

Consider a series of functions ∑' n, f n x. If all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable. Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise convergence then the series is zero everywhere so the result still holds.

theorem fderiv_tsum_apply {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {x₀ : E} (hu : Summable u) (hf : ∀ (n : α), Differentiable 𝕜 (f n)) (hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n) (hf0 : Summable fun (n : α) => f n x₀) (x : E) : fderiv 𝕜 (fun (y : E) => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x

theorem deriv_tsum_apply {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {y₀ : 𝕜} (hu : Summable u) (hg : ∀ (n : α), Differentiable 𝕜 (g n)) (hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n) (hg0 : Summable fun (n : α) => g n y₀) (y : 𝕜) : deriv (fun (z : 𝕜) => ∑' (n : α), g n z) y = ∑' (n : α), deriv (g n) y

theorem fderiv_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {x₀ : E} (hu : Summable u) (hf : ∀ (n : α), Differentiable 𝕜 (f n)) (hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n) (hf0 : Summable fun (n : α) => f n x₀) : (fderiv 𝕜 fun (y : E) => ∑' (n : α), f n y) = fun (x : E) => ∑' (n : α), fderiv 𝕜 (f n) x

theorem deriv_tsum {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {g : α → 𝕜 → F} {y₀ : 𝕜} (hu : Summable u) (hg : ∀ (n : α), Differentiable 𝕜 (g n)) (hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n) (hg0 : Summable fun (n : α) => g n y₀) : (deriv fun (y : 𝕜) => ∑' (n : α), g n y) = fun (y : 𝕜) => ∑' (n : α), deriv (g n) y

Higher smoothness

theorem iteratedFDeriv_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞} (hf : ∀ (i : α), ContDiff 𝕜 N (f i)) (hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)) (h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ} (hk : ↑k ≤ N) : (iteratedFDeriv 𝕜 k fun (y : E) => ∑' (n : α), f n y) = fun (x : E) => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x

Consider a series of smooth functions, with summable uniform bounds on the successive derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative.

theorem iteratedFDeriv_tsum_apply {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞} (hf : ∀ (i : α), ContDiff 𝕜 N (f i)) (hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)) (h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ} (hk : ↑k ≤ N) (x : E) : iteratedFDeriv 𝕜 k (fun (y : E) => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x

Consider a series of smooth functions, with summable uniform bounds on the successive derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative.

theorem contDiff_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞} (hf : ∀ (i : α), ContDiff 𝕜 N (f i)) (hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)) (h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) : ContDiff 𝕜 N fun (x : E) => ∑' (i : α), f i x

Consider a series of functions ∑' i, f i x. Assume that each individual function f i is of class C^N, and moreover there is a uniform summable upper bound on the k-th derivative for each k ≤ N. Then the series is also C^N.

theorem contDiff_tsum_of_eventually {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞} (hf : ∀ (i : α), ContDiff 𝕜 N (f i)) (hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)) (h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in Filter.cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) : ContDiff 𝕜 N fun (x : E) => ∑' (i : α), f i x

Consider a series of functions ∑' i, f i x. Assume that each individual function f i is of class C^N, and moreover there is a uniform summable upper bound on the k-th derivative for each k ≤ N (except maybe for finitely many is). Then the series is also C^N.