Smoothness of series

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

More specifically,

• continuous_tsum ensures that a series of continuous functions is continuous.
• 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.

Continuity

theorem tendstoUniformlyOn_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} {f : α → β → F} (hu : Summable u) {s : Set β} (hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) : TendstoUniformlyOn (fun (t : Finset α) (x : β) => Finset.sum t fun (n : α) => f n x) (fun (x : β) => ∑' (n : α), f n x) Filter.atTop s

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version relative to a set, with general index set.

theorem tendstoUniformlyOn_tsum_nat {β : Type u_2} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set β} (hfu : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ u n) : TendstoUniformlyOn (fun (N : ℕ) (x : β) => Finset.sum (Finset.range N) fun (n : ℕ) => f n x) (fun (x : β) => ∑' (n : ℕ), f n x) Filter.atTop s

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version relative to a set, with index set ℕ.

theorem tendstoUniformly_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} {f : α → β → F} (hu : Summable u) (hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n) : TendstoUniformly (fun (t : Finset α) (x : β) => Finset.sum t fun (n : α) => f n x) (fun (x : β) => ∑' (n : α), f n x) Filter.atTop

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version with general index set.

theorem tendstoUniformly_tsum_nat {β : Type u_2} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) (hfu : ∀ (n : ℕ) (x : β), ‖f n x‖ ≤ u n) : TendstoUniformly (fun (N : ℕ) (x : β) => Finset.sum (Finset.range N) fun (n : ℕ) => f n x) (fun (x : β) => ∑' (n : ℕ), f n x) Filter.atTop

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version with index set ℕ.

theorem continuousOn_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [TopologicalSpace β] {f : α → β → F} {s : Set β} (hf : ∀ (i : α), ContinuousOn (f i) s) (hu : Summable u) (hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) : ContinuousOn (fun (x : β) => ∑' (n : α), f n x) s

An infinite sum of functions with summable sup norm is continuous on a set if each individual function is.

theorem continuous_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [TopologicalSpace β] {f : α → β → F} (hf : ∀ (i : α), Continuous (f i)) (hu : Summable u) (hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n) : Continuous fun (x : β) => ∑' (n : α), f n x

An infinite sum of functions with summable sup norm is continuous if each individual function is.

Differentiability

theorem summable_of_summable_hasFDerivAt_of_isPreconnected {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set 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₀) {x : E} (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 hasFDerivAt_tsum_of_isPreconnected {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [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 summable_of_summable_hasFDerivAt {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [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 hasFDerivAt_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [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 differentiable_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [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 fderiv_tsum_apply {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [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 fderiv_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F} (hu : Summable u) (hf : ∀ (n : α), Differentiable 𝕜 (f n)) (hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n) {x₀ : E} (hf0 : Summable fun (n : α) => f n x₀) : (fderiv 𝕜 fun (y : E) => ∑' (n : α), f n y) = fun (x : E) => ∑' (n : α), fderiv 𝕜 (f n) x

Higher smoothness

theorem iteratedFDeriv_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [IsROrC 𝕜] [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} [IsROrC 𝕜] [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} [IsROrC 𝕜] [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} [IsROrC 𝕜] [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.