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,
continuous_tsumensures that a series of continuous functions is continuous.differentiable_tsumensures that a series of differentiable functions is differentiable.cont_diff_tsumensures that a series of smooth functions is smooth.
We also give versions of these statements which are localized to a set.
Continuity #
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.
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 ℕ.
An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version with general index set.
An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with index set ℕ.
An infinite sum of functions with summable sup norm is continuous on a set if each individual function is.
An infinite sum of functions with summable sup norm is continuous if each individual function is.
Differentiability #
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.
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.
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.
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.
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.
Higher smoothness #
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.
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.
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.
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.