continuousOn_tsum
theorem continuousOn_tsum :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : CompleteSpace F] {u : α → ℝ}
[inst_2 : TopologicalSpace β] {f : α → β → F} {s : Set β},
(∀ (i : α), ContinuousOn (f i) s) →
Summable u → (∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) → ContinuousOn (fun x => ∑' (n : α), f n x) s
This theorem states that for any types `α` (indexing the sequence of functions), `β` (domain of the functions), and `F` (codomain of the functions), where `F` is a normed additive commutative group and a complete space, given a function `u` from `α` to the real numbers, a topological space structure on `β`, a sequence of functions `f` indexed by `α` from `β` to `F`, and a set `s` of elements of type `β`, if each function in the sequence is continuous on the set `s`, the function `u` is summable, and for each function in the sequence and each element in the set `s`, the norm of the value of the function at that element is less than or equal to the corresponding value of `u`, then the function defined by the infinite sum of the sequence of functions, evaluated at each point, is also continuous on the set `s`. In mathematical terms, this theorem states that an infinite sum of continuous functions, each bounded by a summable sequence, is also a continuous function.
More concisely: If `α` is a type, `β` is a topological space, `F` is a normed additive commutative group and complete space, `u : α → ℝ`, `f : α → β → F`, `s : set β`, `u` is summable, each `f(i)` is continuous on `s`, and for all `i ∈ α` and `x ∈ s`, `||f(i)(x)|| ≤ |u(i)|`, then the function `g : β → F` defined by `g(x) := Σi : α. u(i) * f(i)(x)` is continuous on `s`.
|
tendstoUniformly_tsum_nat
theorem tendstoUniformly_tsum_nat :
∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : CompleteSpace F] {f : ℕ → β → F}
{u : ℕ → ℝ},
Summable u →
(∀ (n : ℕ) (x : β), ‖f n x‖ ≤ u n) →
TendstoUniformly (fun N x => (Finset.range N).sum fun n => f n x) (fun x => ∑' (n : ℕ), f n x) Filter.atTop
This theorem states that for a series of functions (f : ℕ → β → F) from natural numbers to some normed additively commutative group (F), if the series has a summable sup norm (u : ℕ → ℝ), then the partial sums of this series (summed over a range from 0 to N) converge uniformly to the infinite sum of the series, as N tends to infinity. This uniform convergence is characterized by the property that for any given "closeness" criteria, there exists a point beyond which the distance between the partial sum and the infinite sum is less than the given criteria, for all x in the domain.
More concisely: If a series of functions from natural numbers to a normed additively commutative group has a summable sup norm, then its partial sums uniformly converge to the infinite sum, ensuring that for any given closeness criteria, the distance between partial sum and infinite sum is less than the given criteria for all domain elements.
|
tendstoUniformly_tsum
theorem tendstoUniformly_tsum :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : CompleteSpace F] {u : α → ℝ}
{f : α → β → F},
Summable u →
(∀ (n : α) (x : β), ‖f n x‖ ≤ u n) →
TendstoUniformly (fun t x => t.sum fun n => f n x) (fun x => ∑' (n : α), f n x) Filter.atTop
The theorem `tendstoUniformly_tsum` states that for any types `α`, `β`, and `F`, with `F` being a normed add commutative group and a complete space, and given two functions `u : α → ℝ` and `f : α → β → F`, if the function `u` is summable and for all `n` in `α` and `x` in `β`, the norm of `f(n, x)` is less than or equal to `u(n)`, then the sequence of partial sums of `f` (obtained by summing over the first `t` elements) converges uniformly to the infinite sum of `f` as `t` goes to infinity. In other words, an infinite sum of functions with a summable supremum norm is the uniform limit of its partial sums. This version of the theorem is applicable to a general index set.
More concisely: If `u` is summable and for all `n` in `α` and `x` in `β`, the norm of `f(n, x)` is less than or equal to `u(n)`, then the sequence of partial sums of the function `F`-valued series `f` converges uniformly to its infinite sum.
|
tendstoUniformlyOn_tsum_nat
theorem tendstoUniformlyOn_tsum_nat :
∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : CompleteSpace F] {f : ℕ → β → F}
{u : ℕ → ℝ},
Summable u →
∀ {s : Set β},
(∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ u n) →
TendstoUniformlyOn (fun N x => (Finset.range N).sum fun n => f n x) (fun x => ∑' (n : ℕ), f n x)
Filter.atTop s
This theorem states that for any sequence of functions `f` mapping natural numbers to a function from `β` to a normed additive commutative group `F`, along with a sequence of real numbers `u` which is summable, and a set `s` of type `β`, if the norm of `f n x` for all `n` and `x` in `s` is less than or equal to `u n`, then the sequence of partial sums of `f` tends to the infinite sum of `f`, uniformly on `s`, as we go to infinity. In other words, an infinite sum of functions `f` with summable supremum norm is the uniform limit of its partial sums, where the partial sums are defined over the set of natural numbers less than `N` (represented by `Finset.range N`), on the set `s`, and the process goes to infinity (`Filter.atTop`).
More concisely: Given a sequence of functions `f` from natural numbers to functions from a set `β` to a normed additive commutative group `F`, with summable supremum norm, and a set `s` in `β`, if the norm of `f n x` is less than or equal to the summable sequence `u` for all `n` and `x` in `s`, then the sequence of partial sums of `f` uniformly converges to the infinite sum of `f` on `s` as `n` goes to infinity.
|
continuous_tsum
theorem continuous_tsum :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : CompleteSpace F] {u : α → ℝ}
[inst_2 : TopologicalSpace β] {f : α → β → F},
(∀ (i : α), Continuous (f i)) →
Summable u → (∀ (n : α) (x : β), ‖f n x‖ ≤ u n) → Continuous fun x => ∑' (n : α), f n x
The theorem `continuous_tsum` states that for any types `α`, `β`, and `F`, where `F` is a normed additive commutative group and a complete space, and for any real-valued function `u` and any function `f` from `α` and `β` to `F`, if every function `f i` is continuous for all `i` in `α`, and if `u` is summable, and if for all `n` in `α` and `x` in `β`, the norm of `f n x` is less than or equal to `u n`, then the function that maps each `x` in `β` to the infinite sum over `α` of `f n x` is continuous. In simpler terms, it states that an infinite sum of functions (each of which is continuous and has a summable sup norm) is also continuous.
More concisely: If `F` is a normed additive commutative group and a complete space, `u` is summable, and each `f i : α × β → F` is continuous with `‖f i(n, x)‖ ≤ u n for all (n : α) and (x : β)`, then the function that maps each `x : β` to the infinite sum over `α` of `f n x` is continuous.
|
tendstoUniformlyOn_tsum
theorem tendstoUniformlyOn_tsum :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : CompleteSpace F] {u : α → ℝ}
{f : α → β → F},
Summable u →
∀ {s : Set β},
(∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) →
TendstoUniformlyOn (fun t x => t.sum fun n => f n x) (fun x => ∑' (n : α), f n x) Filter.atTop s
This theorem states that, given a type of functions `F` that form a normed additive commutative group and a complete space, a function mapping `α` to real numbers `u`, and a function `f` mapping `α` and `β` to `F`, if `u` is summable, then for any set `s` of type `β`, if for all `n` of type `α`, and for all `x` in `s`, the norm of `f n x` is less than or equal to `u n`, then the sequence of partial sums of `f` (represented as `∑ x in t, f x`) converges uniformly to the infinite sum of `f` (represented as `∑' (n : α), f n x`) as `t` tends to infinity, meaning that the difference between the partial sum and the infinite sum can be made arbitrarily small by choosing a sufficiently large `t`.
In other words, an infinite series of functions whose supremum norm is summable uniformly converges to its infinite sum on a given set, with respect to the filter at infinity. More formally, for any entourage of the diagonal `u` in the uniformity of `F`, after a certain index `t`, for all `x` in the set, the distance between the infinite sum and the partial sum up to `t` is smaller than the entourage `u`.
More concisely: Given a normed additive commutative group of functions `F`, a complete space, a summable function `u` to real numbers, and a function `f` mapping `α × β` to `F`, if for all `x` in every set `s` of type `β`, the norm of `f n x` is less than or equal to `u n` for all `n` of type `α`, then the sequence of partial sums of `f` uniformly converges to the infinite sum of `f` as `t` approaches infinity.
|