HasSum.prod_fiberwise
theorem HasSum.prod_fiberwise :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : ContinuousAdd α] [inst_3 : RegularSpace α] {f : β × γ → α} {g : β → α} {a : α},
HasSum f a → (∀ (b : β), HasSum (fun c => f (b, c)) (g b)) → HasSum g a
The theorem states that if we have a series `f` which is defined on the product of two types `β` and `γ` with sum `a`, and for each element `b` of type `β`, the series `f` restricted to `{b} × γ` (which is a cross product of the singleton set `{b}` and `γ`) has sum `g b`, then the series `g` will also have sum `a`. This theorem holds for any types `α`, `β`, and `γ` provided `α` is an additive commutative monoid, a topological space, supports continuous addition, and is a regular space.
More concisely: Given a series `f` on the product of additive commutative monoid and topological space `α × βγ`, where `βγ` is the product of types `β` and `γ`, such that for each `b ∈ β`, the series `f` restricted to `{b} × γ` has sum `g b`, then `g` has sum equal to the sum of `f`.
|
tsum_prod'
theorem tsum_prod' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : ContinuousAdd α] [inst_3 : T3Space α] {f : β × γ → α},
Summable f → (∀ (b : β), Summable fun c => f (b, c)) → ∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
This theorem is about the summation of a function that takes pairs of values as input. Specifically, it states that for any types `α`, `β`, and `γ`, given `α` is an additive commutative monoid and a topological space, and addition operation on `α` is continuous, if a function `f` from pairs of `β` and `γ` to `α` is summable, and for all `b` in `β`, the function obtained by fixing the first argument of `f` to `b` is also summable, then the infinite sum over all pairs `(b, c)` of `f` equals to the double infinite sum over `b` and `c` of `f`. This is a property of rearranging terms in infinite sums, and it relies on the assumption that the original sum and the terms obtained by fixing the first argument of function are all summable.
More concisely: Let `α` be an additive commutative monoid and topological space with continuous addition, and let `f : β × γ → α` be a summable function such that for all `b ∈ β`, the function `x => f (b, x)` is also summable. Then the infinite sum of `f` equals the double infinite sum over `b` and `c` of `f (b, c)`.
|
Pi.summable
theorem Pi.summable :
∀ {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [inst : (x : α) → AddCommMonoid (π x)]
[inst_1 : (x : α) → TopologicalSpace (π x)] {f : ι → (x : α) → π x},
Summable f ↔ ∀ (x : α), Summable fun i => f i x
The theorem `Pi.summable` states that for all types `α`, `ι`, and a type function `π` from `α` to some type; given an additive commutative monoid structure and a topological space structure for every element of type `α`; and a function `f` from `ι` to a function mapping `α` to `π x`, `f` is summable if and only if for every `x` of type `α`, the function `f i x` is summable. Here, `Summable f` denotes the existence of an (possibly infinite) sum for the function `f`.
More concisely: For a function `f` from an index type `ι` to functions from type `α` to a summable type `π`, `f` is summable if and only if for all `x` in `α`, the function `f i x` is summable.
|
tsum_sigma'
theorem tsum_sigma' :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : ContinuousAdd α]
[inst_3 : T3Space α] {γ : β → Type u_5} {f : (b : β) × γ b → α},
(∀ (b : β), Summable fun c => f ⟨b, c⟩) →
Summable f → ∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
The `tsum_sigma'` theorem states that for all types `α`, `β`, and a type function `γ` defined on `β`, given `α` is an additive commutative monoid, a topological space, supports continuous addition, and is a T3 space, and given a function `f` that maps each pair of type `β` and type `γ b` to `α`, if the sum of the function `f` is defined (is summable) for every `b` of type `β`, and overall is also summable, then the total sum of `f` over each pair of type `β` and `γ b` is equal to the sum of `f` over each `b` of type `β` and each `c` of type `γ b`. In mathematical terms, $\sum' (p : (b : β) × γ b), f(p) = \sum' (b : β) (c : γ b), f(b, c)$.
More concisely: Given a commutative additive monoid `α` that is a T3 topological space supporting continuous addition, a function `f` from `β × γ b` to `α` is summable if and only if it is summable component-wise, i.e., the sum of `f` over all pairs is equal to the sum over all elements of `β` and their corresponding elements of `γ b`.
|
tsum_comm'
theorem tsum_comm' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : ContinuousAdd α] [inst_3 : T3Space α] {f : β → γ → α},
Summable (Function.uncurry f) →
(∀ (b : β), Summable (f b)) →
(∀ (c : γ), Summable fun b => f b c) → ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
This theorem, named `tsum_comm'`, states that under certain conditions, the order of summation can be interchanged for a double infinite series. These conditions are:
- The function `f` taking two inputs from sets of types `β` and `γ` respectively, and producing a value of type `α`, can be uncurried to become a function that takes a pair of values as an input.
- The function `f`, after being uncurried, is summable. This means that the infinite sum of the function `f` over its domain exists.
- For every value of `b` in type `β`, the series over `γ` is summable.
- For every value of `c` in type `γ`, the series over `β` is summable.
If these conditions hold, the theorem states that the double series can be summed in any order: summing first over `γ` and then over `β` produces the same result as summing first over `β` and then over `γ`. In mathematical terms, ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c.
More concisely: If functions `f` meeting certain uncurriability and summability conditions are applied to double indices `(b : β, c : γ)`, then interchanging the order of summation over `β` and `γ` yields the same result: `∑' b ∑' c f b c = ∑' c ∑' b f b c`.
|
tsum_apply
theorem tsum_apply :
∀ {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [inst : (x : α) → AddCommMonoid (π x)]
[inst_1 : (x : α) → TopologicalSpace (π x)] [inst_2 : ∀ (x : α), T2Space (π x)] {f : ι → (x : α) → π x} {x : α},
Summable f → tsum (fun i => f i) x = ∑' (i : ι), f i x
This theorem states that for any types `α`, `ι`, and `π`, where `π` is a function from `α` to some type, and for any operations of addition and topology on `π x` (for each `x` in `α`), and assuming `π x` is a Hausdorff space (or T2 space) for each `x` in `α`, then for any function `f` from `ι` to `π x` (for each `x` in `α`) and any element `x` in `α`, if `f` is summable, the sum over `ι` of `f i` at the point `x` is equal to the total sum of the function `f` at the point `x`.
In other words, if we have a function `f` that is mapping from `ι` to some value in `π x` (for a given `x`), and if that function `f` has a sum, the sum over all elements in `ι` of the function applied to those elements is the same as the total sum of the function at that point `x`.
More concisely: Given types `α`, `ι`, and a Hausdorff space `π` over `α`, if `π x` has additions and `f` is a summable function from `ι` to `π x` for each `x` in `α`, then for all `x` in `α`, the sum of `f i` over `ι` equals the total sum of `f` at `x`.
|
HasSum.unop
theorem HasSum.unop :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ},
HasSum f a → HasSum (fun a => (f a).unop) a.unop
The theorem `HasSum.unop` states that for any types `α` and `β`, where `α` is an additive commutative monoid and has a topological structure, if a function `f : β → αᵐᵒᵖ` (from `β` to the multiplicative opposite of `α`) has a sum `a` (i.e., the series formed by `f` sums up to `a`), then the function obtained by applying the operation `MulOpposite.unop` (which transforms elements from the multiplicative opposite space back to `α`) to `f` also has a sum, which is the `MulOpposite.unop` of `a`. In other words, summing the elements in the original space `α` gives the same result as summing their opposites and then taking the opposite of the sum.
More concisely: For any additive commutative monoid `α` with a topological structure and any function `f : β → αᵐᵒᵖ` from `β` to the multiplicative opposite of `α`, if the series formed by `f` sums up to an element `a` in the multiplicative opposite space, then the series formed by applying `MulOpposite.unop` to the elements of `f` sums up to `MulOpposite.unop(a)` in `α`.
|
HasSum.sigma
theorem HasSum.sigma :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : ContinuousAdd α]
[inst_3 : RegularSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} {g : β → α} {a : α},
HasSum f a → (∀ (b : β), HasSum (fun c => f ⟨b, c⟩) (g b)) → HasSum g a
This theorem states that for any types `α`, `β`, and a type function `γ` on `β`, given a function `f` mapping from a pair of `β` and `γ b` to `α`, a function `g` mapping from `β` to `α`, and a value `a` of type `α`, if `f` has a sum of `a` and for all values of `β`, the function `f` with fixed `β` and varying `γ b` has a sum of `g b`, then `g` has a sum of `a`.
Here, `HasSum f a` means that the series formed by `f` is summable and its sum is `a`. The prerequisites such as `AddCommMonoid α`, `TopologicalSpace α`, `ContinuousAdd α`, and `RegularSpace α` are necessary mathematical structures and conditions to ensure that the notion of summation is well-defined and continuous in the context of the topological space `α`.
More concisely: If for any type `β` and a type function `γ` on `β`, given a function `f` from the product of `β` and `γ b` to `α` such that for all `β` and `γ b`, `HasSum (λ x := f x (γ b)) (g b)`, and there exists an element `a` of type `α` such that `HasSum f a`, then `HasSum g a`.
|
Summable.sigma_factor
theorem Summable.sigma_factor :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : UniformAddGroup α]
[inst_3 : CompleteSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α},
Summable f → ∀ (b : β), Summable fun c => f ⟨b, c⟩
The theorem `Summable.sigma_factor` states that for any types `α` and `β`, any additive commutative group structure on `α`, and a uniform space and uniform additive group structure on `α` where `α` is complete, given a function `f` from the cartesian product of `β` and a type `γ` dependent on `β` to `α` that is summable (i.e., the infinite sum of `f` exists), then for each fixed `b` in `β`, the function `f` applied to the pair `(b, c)` is also summable over all `c` in the type `γ b`. Essentially, it asserts that if an infinite sum over a dependent pair type exists, then the infinite sum over each "slice" of the dependent pair type also exists.
More concisely: For any additive commutative group `α` with a complete uniform structure, and a summable function `f : β × γ → α`, the function `f` is summable for each fixed `b ∈ β` over the dependent type `γ b`.
|
HasSum.op
theorem HasSum.op :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α},
HasSum f a → HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a)
This theorem, named `HasSum.op`, says that for any types `α` and `β` where `α` is an additive commutative monoid and also has a topological space structure, and for any function `f` from `β` to `α` and any element `a` of `α`, if the series defined by `f` has a sum equal to `a`, then the series defined by the function which applies the operation `MulOpposite.op` to `f(a)` also has a sum, and this sum is equal to the opposite of `a` under the `MulOpposite.op` operation. In other words, the sum of the `MulOpposite.op` applied series is the `MulOpposite.op` of the sum of the original series.
More concisely: For any additive commutative monoid `α` with a topological space structure and function `f: β → α`, if the series defined by `f` sums to an element `a` in `α`, then the series defined by `MulOpposite.op ∘ f` sums to `MulOpposite.op a`.
|