HasSum.int_rec
theorem HasSum.int_rec :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [inst_2 : ContinuousAdd M]
{f g : ℕ → M}, HasSum f m → HasSum g m' → HasSum (fun t => Int.rec f g t) (m + m')
The theorem `HasSum.int_rec` is about the summation of two sequences in a certain topology. It states that if you have two sequences `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` that sum up to values `a` and `b` respectively, then if you create a new sequence by placing `f₀` at the `0`-th position and aligning the `f` and `g` sequences on either side of it (`..., g₂, g₁, g₀, f₀, f₁, f₂, ...`), this new sequence will have a sum of `a + b`. This applies to any type `M` that is a topological space and has addition, given the addition operation is continuous.
More concisely: If `(M, +)` is a topological space with continuous addition and `(f\_n)` and `(g\_n)` are sequences in `M` such that `∑(i=0)^∞ f\_i = a` and `∑(i=0)^∞ g\_i = b`, then `∑(i=-\infty)^∞ (if i ≤ 0 then g\_i else f\_i) = a + b`.
|
rel_iSup_tsum
theorem rel_iSup_tsum :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
[inst_2 : Countable β] [inst_3 : CompleteLattice α] (m : α → M),
m ⊥ = 0 →
∀ (R : M → M → Prop),
(∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) →
∀ (s : β → α), R (m (⨆ b, s b)) (∑' (b : β), m (s b))
The theorem `rel_iSup_tsum` states that for any type `M` with an additive commutative monoid structure and a topological space structure, any countable type `β`, and any complete lattice type `α`, if a function `m` from `α` to `M` satisfies that `m` of the least element is zero, and for every sequence of `α` indexed by natural numbers, the function `m` is countably sub-additive (meaning that the `m` of the supremum is less than or equal to the sum of `m` of the sequence elements), then this sub-additivity property holds for any sequence of `α` indexed by the countable type `β`. This theorem essentially generalizes the countable sub-additivity property from sequences indexed by natural numbers to sequences indexed by any countable type.
More concisely: For any additive commutative monoid M with a topological space structure, complete lattice α, and countable type β, if the function m from α to M with m(∥0∥) = 0 satisfies countable sub-additivity for sequences indexed by natural numbers, then it also satisfies countable sub-additivity for sequences indexed by β.
|
sum_add_tsum_nat_add'
theorem sum_add_tsum_nat_add' :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : T2Space M]
[inst_3 : ContinuousAdd M] {f : ℕ → M} {k : ℕ},
(Summable fun n => f (n + k)) → ((Finset.range k).sum fun i => f i) + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
This theorem states that for any type `M` that has an additive commutative monoid structure, a topological space structure, a Hausdorff (`T2Space`) structure, and a structure of continuous addition, along with a function `f` from natural numbers to `M` and a natural number `k`, if the function `f` applied to `n + k` (for all natural numbers `n`) is summable, then the sum of `f(i)` for `i` in the range from 0 to `k-1` plus the sum of `f(i + k)` for all natural numbers `i` is equal to the sum of `f(i)` for all natural numbers `i`. In mathematical terms, it states $\sum_{i=0}^{k-1} f(i) + \sum_{i=0}^{\infty} f(i + k) = \sum_{i=0}^{\infty} f(i)$.
More concisely: For any additive commutative monoid `M` with topological space, Hausdorff space, continuous addition structures, and a summable function `f` from natural numbers to `M`, the sum of `f(i)` for `i` from 0 to `k-1` and the sum of `f(i+k)` for all `i` equals the infinite sum of `f(i)`.
|
sum_add_tsum_nat_add
theorem sum_add_tsum_nat_add :
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
[inst_3 : T2Space G] {f : ℕ → G} (k : ℕ),
Summable f → ((Finset.range k).sum fun i => f i) + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
The theorem `sum_add_tsum_nat_add` states that for any type `G` that has the structure of an additive commutative group, a topological space, a topological additive group, and a T2 space (also known as a Hausdorff space), and for any function `f` from the natural numbers to `G`, if `f` is summable, then the sum of `f` over the set of natural numbers less than a given number `k`, plus the infinite sum of `f` applied to each natural number `i` increased by `k`, is equal to the infinite sum of `f` over all the natural numbers. This theorem essentially states a shifting property of the infinite sum of a summable sequence.
More concisely: For any summable function `f` from natural numbers to an additive commutative group `G` in a T2 topological space with the structure of a topological additive group, the sum of `f` over the first `k` natural numbers and the infinite sum of `f` shifted by `k` are equal.
|
hasSum_nat_add_iff
theorem hasSum_nat_add_iff :
∀ {G : Type u_2} [inst : AddCommGroup G] {g : G} [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
{f : ℕ → G} (k : ℕ), HasSum (fun n => f (n + k)) g ↔ HasSum f (g + (Finset.range k).sum fun i => f i)
The theorem `hasSum_nat_add_iff` states that for any type `G` which is an additive commutative group and a topological additive group, any function `f` from natural numbers to `G`, and any natural number `k`, the sum of the sequence `f(n + k)` has a limit `g` if and only if the function `f` has a limit equal to `g` plus the sum of the function `f` applied to the range from `0` to `k - 1`. In mathematical terms, this theorem asserts that $\sum_{n=0}^\infty f(n + k) = g$ if and only if $\sum_{n=0}^\infty f(n) = g + \sum_{i=0}^{k-1} f(i)$. This effectively means shifting the start of the sequence by `k` entries does not change the sum, but it does change the value to which the series converges.
More concisely: For any additive commutative and topological group G, function f from natural numbers to G, and natural number k, if the sequence (f(n + k)) has a limit g, then f has a limit g + ∑(i=0 to k-1) f(i).
|
HasSum.tendsto_sum_nat
theorem HasSum.tendsto_sum_nat :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℕ → M},
HasSum f m → Filter.Tendsto (fun n => (Finset.range n).sum fun i => f i) Filter.atTop (nhds m)
This theorem states that if a function `f` from natural numbers to a type `M` has a sum `m`, then the partial sums `∑ i in range n, f i`, where the range is a set of natural numbers less than `n`, converge to `m` as `n` goes to infinity. Here, `M` is a type that forms an additive commutative monoid and also has a topological space structure. The convergence is expressed in terms of filters: `Filter.Tendsto` is used to assert that the limit of the sequence of partial sums (considered as a function of `n`) as `n` goes to infinity (represented by `Filter.atTop`) is `m` (represented by the neighborhood filter `nhds m`).
More concisely: If `f` is a function from natural numbers to an additive commutative monoid and topological space `M`, with `m` being the sum of `f` over finite natural number sets and `n` tending to infinity, then `∑ i in range n, f i` converges to `m` in the sense of `Filter.Tendsto` as `n` approaches infinity.
|
tsum_iSup_decode₂
theorem tsum_iSup_decode₂ :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
[inst_2 : Encodable β] [inst_3 : CompleteLattice α] (m : α → M),
m ⊥ = 0 → ∀ (s : β → α), ∑' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ β i, s b) = ∑' (b : β), m (s b)
The theorem `tsum_iSup_decode₂` states the following in the context of an abstract algebra:
Given a type `M` that is an additive commutative monoid and a topological space, a type `β` that is encodable, a type `α` that is a complete lattice, a function `m` from `α` to `M` such that `m` at the bottom element of the lattice is 0, and a function `s` from `β` to `α`, the sum over all natural numbers of `m` applied to the supremum over all `b` in the preimage of `i` under the decoding function, of `s` applied to `b`, is equal to the sum over all `b` in `β` of `m` applied to `s` applied to `b`.
In simpler terms, we can compute a sum over an encodable type by summing over the natural numbers and taking a supremum. This is particularly useful in the context of outer measures.
More concisely: For an additive commutative monoid M in a topological space, a complete lattice α, encodable type β, function m : α → M with m(⊥) = 0, and function s : β → α, the sum of m(sup {s(b) | b ∈ preimage i of decoding function}) for all natural numbers i, equals the sum of m(s(b)) for all b in β.
|
summable_nat_add_iff
theorem summable_nat_add_iff :
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G] {f : ℕ → G}
(k : ℕ), (Summable fun n => f (n + k)) ↔ Summable f
The theorem `summable_nat_add_iff` states that for any type `G` which forms an additive commutative group, a topological space, and also a topological additive group, and for any function `f` from natural numbers to `G`, and for any natural number `k`, the statement that the function `f` shifted by `k` (i.e., `f(n + k)` for all natural numbers `n`) is summable if and only if the original function `f` is summable. Here, a function is said to be summable if the series formed by its values has a sum in the topological space.
More concisely: For any additive commutative group G that is a topological space and topological additive group, and for any function f from natural numbers to G, the shifted function f(n + k) is summable if and only if the original function f is summable.
|
rel_iSup_sum
theorem rel_iSup_sum :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {γ : Type u_5}
[inst_2 : CompleteLattice α] (m : α → M),
m ⊥ = 0 →
∀ (R : M → M → Prop),
(∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) →
∀ (s : γ → α) (t : Finset γ), R (m (⨆ d ∈ t, s d)) (t.sum fun d => m (s d))
This theorem states that if a function `m` is countably sub-additive, then it is sub-additive on finite sets. More specifically, given a function `m` from a complete lattice `α` to a topological monoid `M` such that `m` of the bottom element of `α` is zero, and a relation `R` under which `m` is countably sub-additive (i.e., for any sequence `s` of elements from `α`, `R` holds between `m` of the supremum of the sequence and the infinite sum of `m` applied to each element of the sequence), then for any function `s` from a type `γ` to `α` and any finite set `t` of `γ`, `R` holds between `m` of the supremum of `s` over the elements in `t` and the sum of `m` applied to `s` of each element in `t`.
More concisely: If a countably sub-additive function from a complete lattice to a topological monoid with zero at the bottom element satisfies the relation between the supremum and infinite sum, then the relation holds between the supremum over a finite set and the sum over the same set.
|
summable_int_of_summable_nat
theorem summable_int_of_summable_nat :
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G] {f : ℤ → G},
(Summable fun n => f ↑n) → (Summable fun n => f (-↑n)) → Summable f
The theorem `summable_int_of_summable_nat` states that for any function `f` from the integers to a topological additive group `G`, if the function `f` summed over the natural numbers is summable and the function `f` summed over the negative natural numbers is also summable, then the function `f` summed over all integers is summable. Here, summability means that there exists a limit to the infinite sum of the sequence produced by the function.
More concisely: If a function from integers to a topological additive group is summable over natural numbers and negative natural numbers, then it is summable over all integers.
|
tsum_iUnion_decode₂
theorem tsum_iUnion_decode₂ :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
[inst_2 : Encodable β] (m : Set α → M),
m ∅ = 0 → ∀ (s : β → Set α), ∑' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ β i, s b) = ∑' (b : β), m (s b)
This theorem, `tsum_iUnion_decode₂`, states that for any types `α`, `β`, and `M`, where `M` is an additive commutative monoid and also has a topological space structure, and `β` is encodable, for any function `m` from the set of elements of type `α` to `M` that maps the empty set to zero, and for any function `s` from `β` to the set of elements of type `α`, the sum over all natural numbers `i` of `m` applied to the union of sets `s b` for `b` in the decoded values of `i` in `β`, is equal to the sum over all elements `b` of `β` of `m` applied to `s b`.
In mathematical terms, this theorem says that $\sum_{i \in \mathbb{N}} m \left( \bigcup_{b \in \text{decode}_2(\beta, i)} s(b) \right) = \sum_{b \in \beta} m(s(b))$ where `decode₂ β i` gives the preimage of `i` under the encoding of `β`, if it exists.
More concisely: For any additive commutative monoid M with a topological space structure, encodable type β, and functions m from the powerset of any type α to M mapping the empty set to zero, and s from β to α, the sum of m applied to the union of sets s(b) over all decoded values b in β is equal to the sum of m applied to each s(b).
|
tendsto_sum_nat_add
theorem tendsto_sum_nat_add :
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G]
[inst_3 : T2Space G] (f : ℕ → G), Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
This theorem asserts that for any function `f` mapping natural numbers to an additive commutative group `G` that is equipped with a topological space structure, a topological additive group structure, and a T2 space (also known as a Hausdorff space), the series sum `∑' k, f (k + i)` tends to zero as `i` tends to infinity. Implicit in this statement is that the function `f` does not need to satisfy a summability condition because, if it did, all such series sums would be zero. In mathematical terms, this statement can be written as $\lim_{i \to \infty} \sum_{k} f(k + i) = 0$.
More concisely: Given a function `f` from natural numbers to an additive commutative group `G` with a T2 topology, the series sum `∑' k, f (k + i)` converges to zero as `i` approaches infinity.
|
Summable.tendsto_atTop_zero
theorem Summable.tendsto_atTop_zero :
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : TopologicalAddGroup G] {f : ℕ → G},
Summable f → Filter.Tendsto f Filter.atTop (nhds 0)
The theorem `Summable.tendsto_atTop_zero` states that for any summable function `f` from the natural numbers to a topological add group `G`, the function `f` tends towards 0 as its argument tends towards infinity. In other words, if `f` is a sequence of elements in `G` such that the series `f(0) + f(1) + f(2) + ...` converges, then for any neighborhood of 0 in `G`, there exists a point beyond which all the terms of the sequence `f` stay within that neighborhood. This is a formalization of one of the properties of convergence of series in analysis.
More concisely: For any summable function from natural numbers to a topological add group, the sequence tends to 0 at infinity, meaning for any neighborhood of 0, there exists a natural number beyond which all terms remain in the neighborhood.
|
rel_sup_add
theorem rel_sup_add :
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} [inst_2 : CompleteLattice α]
(m : α → M),
m ⊥ = 0 →
∀ (R : M → M → Prop),
(∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) → ∀ (s₁ s₂ : α), R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)
The theorem `rel_sup_add` states that for any types `M` and `α`, given `M` is an additive commutative monoid and a topological space, and `α` is a complete lattice, if a function `m` from `α` to `M` satisfies that `m` of the bottom element is zero, then for any relation `R` on `M`, if `R` holds for the function value of the supremum of a countable sequence and the sum of the function values of the sequence elements, then `R` also holds for the function value of the supremum of any two elements and the sum of their function values. This essentially states that if a function is countably sub-additive, then it is also binary sub-additive.
More concisely: If `m` is a countably sub-additive function from a complete lattice `α` to an additive commutative monoid and topological space `M`, such that `m` maps the bottom element to zero, then `m` is binary sub-additive.
|