mathlib3 documentation

analysis.calculus.series

Smoothness of series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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,

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

Continuity #

theorem tendsto_uniformly_on_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [normed_add_comm_group F] [complete_space F] {u : α } {f : α β F} (hu : summable u) {s : set β} (hfu : (n : α) (x : β), x s f n x u n) :
tendsto_uniformly_on (λ (t : finset α) (x : β), t.sum (λ (n : α), f n x)) (λ (x : β), ∑' (n : α), f n x) filter.at_top 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 tendsto_uniformly_on_tsum_nat {β : Type u_2} {F : Type u_5} [normed_add_comm_group F] [complete_space F] {f : β F} {u : } (hu : summable u) {s : set β} (hfu : (n : ) (x : β), x s f n x u n) :
tendsto_uniformly_on (λ (N : ) (x : β), (finset.range N).sum (λ (n : ), f n x)) (λ (x : β), ∑' (n : ), f n x) filter.at_top 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 tendsto_uniformly_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [normed_add_comm_group F] [complete_space F] {u : α } {f : α β F} (hu : summable u) (hfu : (n : α) (x : β), f n x u n) :
tendsto_uniformly (λ (t : finset α) (x : β), t.sum (λ (n : α), f n x)) (λ (x : β), ∑' (n : α), f n x) filter.at_top

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

theorem tendsto_uniformly_tsum_nat {β : Type u_2} {F : Type u_5} [normed_add_comm_group F] [complete_space F] {f : β F} {u : } (hu : summable u) (hfu : (n : ) (x : β), f n x u n) :
tendsto_uniformly (λ (N : ) (x : β), (finset.range N).sum (λ (n : ), f n x)) (λ (x : β), ∑' (n : ), f n x) filter.at_top

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

theorem continuous_on_tsum {α : Type u_1} {β : Type u_2} {F : Type u_5} [normed_add_comm_group F] [complete_space F] {u : α } [topological_space β] {f : α β F} {s : set β} (hf : (i : α), continuous_on (f i) s) (hu : summable u) (hfu : (n : α) (x : β), x s f n x u n) :
continuous_on (λ (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} [normed_add_comm_group F] [complete_space F] {u : α } [topological_space β] {f : α β F} (hf : (i : α), continuous (f i)) (hu : summable u) (hfu : (n : α) (x : β), f n x u n) :
continuous (λ (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_has_fderiv_at_of_is_preconnected {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 F] {f : α E F} {f' : α E (E →L[𝕜] F)} {s : set E} {x₀ : E} (hu : summable u) (hs : is_open s) (h's : is_preconnected s) (hf : (n : α) (x : E), x s has_fderiv_at (f n) (f' n x) x) (hf' : (n : α) (x : E), x s f' n x u n) (hx₀ : x₀ s) (hf0 : summable (λ (n : α), f n x₀)) {x : E} (hx : x s) :
summable (λ (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 has_fderiv_at_tsum_of_is_preconnected {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 F] {f : α E F} {f' : α E (E →L[𝕜] F)} {s : set E} {x₀ x : E} (hu : summable u) (hs : is_open s) (h's : is_preconnected s) (hf : (n : α) (x : E), x s has_fderiv_at (f n) (f' n x) x) (hf' : (n : α) (x : E), x s f' n x u n) (hx₀ : x₀ s) (hf0 : summable (λ (n : α), f n x₀)) (hx : x s) :
has_fderiv_at (λ (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_has_fderiv_at {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 F] {f : α E F} {f' : α E (E →L[𝕜] F)} {x₀ : E} (hu : summable u) (hf : (n : α) (x : E), has_fderiv_at (f n) (f' n x) x) (hf' : (n : α) (x : E), f' n x u n) (hf0 : summable (λ (n : α), f n x₀)) (x : E) :
summable (λ (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 has_fderiv_at_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 F] {f : α E F} {f' : α E (E →L[𝕜] F)} {x₀ : E} (hu : summable u) (hf : (n : α) (x : E), has_fderiv_at (f n) (f' n x) x) (hf' : (n : α) (x : E), f' n x u n) (hf0 : summable (λ (n : α), f n x₀)) (x : E) :
has_fderiv_at (λ (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} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 F] {f : α E F} {f' : α E (E →L[𝕜] F)} (hu : summable u) (hf : (n : α) (x : E), has_fderiv_at (f n) (f' n x) x) (hf' : (n : α) (x : E), f' n x u n) :
differentiable 𝕜 (λ (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} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 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 (λ (n : α), f n x₀)) (x : E) :
fderiv 𝕜 (λ (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} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] {u : α } [normed_space 𝕜 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 (λ (n : α), f n x₀)) :
fderiv 𝕜 (λ (y : E), ∑' (n : α), f n y) = λ (x : E), ∑' (n : α), fderiv 𝕜 (f n) x

Higher smoothness #

theorem iterated_fderiv_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] [normed_space 𝕜 F] {f : α E F} {v : α } {N : ℕ∞} (hf : (i : α), cont_diff 𝕜 N (f i)) (hv : (k : ), k N summable (v k)) (h'f : (k : ) (i : α) (x : E), k N iterated_fderiv 𝕜 k (f i) x v k i) {k : } (hk : k N) :
iterated_fderiv 𝕜 k (λ (y : E), ∑' (n : α), f n y) = λ (x : E), ∑' (n : α), iterated_fderiv 𝕜 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 iterated_fderiv_tsum_apply {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] [normed_space 𝕜 F] {f : α E F} {v : α } {N : ℕ∞} (hf : (i : α), cont_diff 𝕜 N (f i)) (hv : (k : ), k N summable (v k)) (h'f : (k : ) (i : α) (x : E), k N iterated_fderiv 𝕜 k (f i) x v k i) {k : } (hk : k N) (x : E) :
iterated_fderiv 𝕜 k (λ (y : E), ∑' (n : α), f n y) x = ∑' (n : α), iterated_fderiv 𝕜 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 cont_diff_tsum {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] [normed_space 𝕜 F] {f : α E F} {v : α } {N : ℕ∞} (hf : (i : α), cont_diff 𝕜 N (f i)) (hv : (k : ), k N summable (v k)) (h'f : (k : ) (i : α) (x : E), k N iterated_fderiv 𝕜 k (f i) x v k i) :
cont_diff 𝕜 N (λ (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 cont_diff_tsum_of_eventually {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [complete_space F] [normed_space 𝕜 F] {f : α E F} {v : α } {N : ℕ∞} (hf : (i : α), cont_diff 𝕜 N (f i)) (hv : (k : ), k N summable (v k)) (h'f : (k : ), k N (∀ᶠ (i : α) in filter.cofinite, (x : E), iterated_fderiv 𝕜 k (f i) x v k i)) :
cont_diff 𝕜 N (λ (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.