Finset.sum_Ico_eq_sub
theorem Finset.sum_Ico_eq_sub :
∀ {δ : Type u_3} [inst : AddCommGroup δ] (f : ℕ → δ) {m n : ℕ},
m ≤ n →
((Finset.Ico m n).sum fun k => f k) = ((Finset.range n).sum fun k => f k) - (Finset.range m).sum fun k => f k
This theorem, `Finset.sum_Ico_eq_sub`, states that for any function `f` from natural numbers to an element of a type `δ` with an additive commutative group structure, and for any natural numbers `m` and `n` such that `m` is less than or equal to `n`, the sum of the function `f` evaluated at each element in the finite integer interval from `m` to `n` (exclusive of `n`) is equal to the difference between the sum of `f` evaluated at each natural number less than `n` and the sum of `f` evaluated at each natural number less than `m`. Essentially, it's relating the sum over an interval to differences of sums over ranges of natural numbers.
More concisely: For any additive commutative group δ and function f from natural numbers to δ, the sum of f over the finite interval [m, n) equals the difference between the sums of f over the intervals [0, m-1] and [0, n-1).
|
Finset.sum_range_reflect
theorem Finset.sum_range_reflect :
∀ {δ : Type u_3} [inst : AddCommMonoid δ] (f : ℕ → δ) (n : ℕ),
((Finset.range n).sum fun j => f (n - 1 - j)) = (Finset.range n).sum fun j => f j
The theorem `Finset.sum_range_reflect` states that for any given natural number `n` and any function `f` from natural numbers to a type `δ` (where `δ` is any type that has an additive commutative monoid structure), the sum of `f(n - 1 - j)`, where `j` ranges over all natural numbers less than `n`, is the same as the sum of `f(j)`, where `j` also ranges over all natural numbers less than `n`. In other words, if we were to take a set of natural numbers less than `n`, and apply the function `f` to each element, the sum of the results would remain unchanged whether we traverse the set in a normal or reverse order.
More concisely: For any natural number `n` and additive commutative monoid homomorphism `f`, the sum of `f(n-1-j)` for `j` ranging from `0` to `n-1` equals the sum of `f(j)` for `j` ranging from `0` to `n-1`.
|
Finset.prod_Ico_succ_top
theorem Finset.prod_Ico_succ_top :
∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ},
a ≤ b → ∀ (f : ℕ → M), ((Finset.Ico a (b + 1)).prod fun k => f k) = ((Finset.Ico a b).prod fun k => f k) * f b
This theorem, `Finset.prod_Ico_succ_top`, states that for any commutative monoid `M`, any natural numbers `a` and `b`, and any function `f` from natural numbers to `M`, if `a` is less than or equal to `b`, then the product of `f(k)` for each `k` in the finite set from `a` to `b+1`, is equal to the product of `f(k)` for each `k` in the finite set from `a` to `b`, multiplied by `f(b)`. This essentially says that adding one more term to the product (when `k` equals `b`) just multiplies the previous product by `f(b)`.
More concisely: For any commutative monoid `M`, function `f` from natural numbers to `M`, and natural numbers `a` and `b` with `a <= b`, the product of `f(k)` for `k` in the finite set from `a` to `b+1` equals the product of `f(k)` for `k` in the finite set from `a` to `b` multiplied by `f(b)`.
|
Finset.sum_range_add_sum_Ico
theorem Finset.sum_range_add_sum_Ico :
∀ {M : Type u_2} [inst : AddCommMonoid M] (f : ℕ → M) {m n : ℕ},
m ≤ n →
(((Finset.range m).sum fun k => f k) + (Finset.Ico m n).sum fun k => f k) = (Finset.range n).sum fun k => f k
The theorem `Finset.sum_range_add_sum_Ico` states that for any type `M` that has a commutative addition operation, any function `f` from natural numbers to `M`, and any two natural numbers `m` and `n` such that `m` is less than or equal to `n`, the sum of `f(k)` for all `k` in the range from `0` to `m-1` plus the sum of `f(k)` for all `k` in the interval `[m, n)` (inclusive of `m` and exclusive of `n`) is equal to the sum of `f(k)` for all `k` in the range from `0` to `n-1`. This theorem essentially states that splitting the sum operation over a range at any point and summing the parts individually yields the same result as summing over the entire range.
More concisely: For any commutative monoid M, function f from natural numbers to M, and natural numbers m ≤ n, the sum of f(k) for k in the range [0, m-1] plus the sum of f(k) for k in the range [m, n) equals the sum of f(k) for k in the range [0, n-1].
|
Finset.sum_range_succ_sub_sum
theorem Finset.sum_range_succ_sub_sum :
∀ {M : Type u_3} (f : ℕ → M) {n : ℕ} [inst : AddCommGroup M],
(((Finset.range (n + 1)).sum fun i => f i) - (Finset.range n).sum fun i => f i) = f n
This theorem, `Finset.sum_range_succ_sub_sum`, states that for any type `M` where `M` is an additive commutative group, and for any function `f` from natural numbers to `M`, and for any natural number `n`, the difference between the sum of `f(i)` over the range `0` to `n + 1` (exclusive) and the sum of `f(i)` over the range `0` to `n` (exclusive) is equal to `f(n)`. In mathematical terms, it states that $\sum_{i=0}^{n+1} f(i) - \sum_{i=0}^{n} f(i) = f(n)$.
More concisely: For any additive commutative group M and function f from natural numbers to M, the sum of f(i) from i=0 to n+1, minus the sum of f(i) from i=0 to n, equals f(n). In symbols, $\sum\_{i=0}^{n+1} f(i) - \sum\_{i=0}^{n} f(i) = f(n)$.
|
Finset.sum_Ico_add'
theorem Finset.sum_Ico_add' :
∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : OrderedCancelAddCommMonoid α]
[inst_2 : ExistsAddOfLE α] [inst_3 : LocallyFiniteOrder α] (f : α → M) (a b c : α),
((Finset.Ico a b).sum fun x => f (x + c)) = (Finset.Ico (a + c) (b + c)).sum fun x => f x
This theorem states that for any type `α` which has a commutative monoid structure with cancellation, an additive structure with a total order such that addition respects the order, and is locally finite, as well as for any type `M` with a commutative monoid structure, and for any function `f` from `α` to `M`, and for any three elements `a`, `b`, and `c` of type `α`, summing the function `f` applied to each element in the interval from `a` to `b` (inclusive of `a`, exclusive of `b`), each incremented by `c`, gives the same result as summing the function `f` over the interval from `a + c` to `b + c` (inclusive of `a + c`, exclusive of `b + c`). In other words, if you shift the interval for the sum by `c`, you get the same result as if you shifted each term in the sum by `c`.
More concisely: For any locally finite commutative monoid `α` with cancellation, a total order, and an additive structure where addition respects the order, and any commutative monoid `M` and function `f` from `α` to `M`, the sum of `f` over the interval `[a, b]` is equal to the sum of `f` over the interval `[a + c, b + c]`, for all `a, b, c` in `α`.
|
Finset.sum_range_id
theorem Finset.sum_range_id : ∀ (n : ℕ), ((Finset.range n).sum fun i => i) = n * (n - 1) / 2
This theorem is a statement of Gauss' summation formula. It says that for any natural number `n`, the sum of all natural numbers less than `n` (obtained using the `Finset.range n` function) is equal to the product of `n` and `n - 1`, divided by 2. In mathematical terms, it's expressing the formula $\sum_{i=0}^{n-1} i = \frac{n*(n-1)}{2}$.
More concisely: The sum of the first `n` natural numbers equals `(n * (n - 1)) / 2`.
|
Mathlib.Algebra.BigOperators.Intervals._auxLemma.3
theorem Mathlib.Algebra.BigOperators.Intervals._auxLemma.3 :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α},
(a ∈ Finset.filter p s) = (a ∈ s ∧ p a)
The theorem `Mathlib.Algebra.BigOperators.Intervals._auxLemma.3` asserts that for any type `α`, any decidable predicate `p` on `α`, any finite set `s` of type `α`, and any element `a` of type `α`, the element `a` belongs to the set `s` filtered by the predicate `p` if and only if `a` belongs to the set `s` and `a` satisfies the predicate `p`. In other words, filtering a finite set by a predicate produces a new set of elements that originally belong to the set and satisfy the predicate.
More concisely: For any type `α`, finite set `s` of `α`, decidable predicate `p` on `α`, and `a` in `s`, `a` is in the set `s` with filter `p` if and only if `a` is in `s` and satisfies `p`.
|
Finset.sum_range_id_mul_two
theorem Finset.sum_range_id_mul_two : ∀ (n : ℕ), ((Finset.range n).sum fun i => i) * 2 = n * (n - 1)
This theorem states Gauss' summation formula for the sum of the first `n` natural numbers. Specifically, it stipulates that the sum of all numbers in the set of natural numbers less than `n` (as defined by `Finset.range n`), when multiplied by 2, equals `n` multiplied by `n - 1`. This is equivalent to the conventional representation of Gauss' formula as $\frac{n(n-1)}{2}$, which forms the sum of an arithmetic series.
More concisely: The sum of the elements in the finite set of natural numbers up to `n` equals `n` times `(n - 1)`.
|
Mathlib.Algebra.BigOperators.Intervals._auxLemma.1
theorem Mathlib.Algebra.BigOperators.Intervals._auxLemma.1 :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : Fintype α] [inst_2 : LocallyFiniteOrderTop α]
[inst_3 : LocallyFiniteOrderBot α] (a : α), {a}ᶜ = (Finset.Ioi a).disjUnion (Finset.Iio a) ⋯
This theorem states that for any type `α` that has a linear order, is a finite type, and has locally finite orders at the top and bottom, the complement of the singleton set `{a}` (i.e., the set of all elements in `α` except `a`) is the disjoint union of the set of elements greater than `a` (`Finset.Ioi a`) and the set of elements less than `a` (`Finset.Iio a`). In other words, any element not in `{a}` is either greater than `a` or less than `a`, and these two sets do not overlap.
More concisely: For any finite, locally ordered type `α` with finite orders at the top and bottom, the complement of a singleton set is the disjoint union of the elements greater than the element in the set and the elements less than it.
|
Finset.sum_Ico_consecutive
theorem Finset.sum_Ico_consecutive :
∀ {M : Type u_2} [inst : AddCommMonoid M] (f : ℕ → M) {m n k : ℕ},
m ≤ n →
n ≤ k →
(((Finset.Ico m n).sum fun i => f i) + (Finset.Ico n k).sum fun i => f i) =
(Finset.Ico m k).sum fun i => f i
The theorem `Finset.sum_Ico_consecutive` states that for any given type `M` that forms an additive commutative monoid and a function `f` from natural numbers to `M`, if we have three natural numbers `m`, `n`, and `k` where `m` is less than or equal to `n` and `n` is less than or equal to `k`, the sum of the function `f` applied over all elements in the inclusive-exclusive interval from `m` to `n` and the sum of the function `f` applied over all elements in the inclusive-exclusive interval from `n` to `k` is equal to the sum of the function `f` applied over all elements in the inclusive-exclusive interval from `m` to `k`. Symbolically, this can be represented as $\sum_{i=m}^{n-1} f(i) + \sum_{i=n}^{k-1} f(i) = \sum_{i=m}^{k-1} f(i)$.
More concisely: For any additive commutative monoid type M and function f from natural numbers to M, the sum of f over consecutive inclusive-exclusive intervals [m, n] and [n, k] equals the sum over the combined interval [m, k]. That is, $\sum\_{i=m}^{n-1} f(i) + \sum\_{i=n}^{k-1} f(i) = \sum\_{i=m}^{k-1} f(i)$.
|
Finset.sum_Ico_Ico_comm
theorem Finset.sum_Ico_Ico_comm :
∀ {M : Type u_3} [inst : AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M),
((Finset.Ico a b).sum fun i => (Finset.Ico i b).sum fun j => f i j) =
(Finset.Ico a b).sum fun j => (Finset.Ico a (j + 1)).sum fun i => f i j
This theorem states that for any additive commutative monoid `M` and any two natural numbers `a` and `b`, the two methods of summing over a function `f : ℕ → ℕ → M` are equivalent when the range of the indices is `a ≤ i ≤ j < b`. The two methods of summation differ in the order of summation: the first sums over `i` first and then `j`, and the second sums over `j` first and then `i`. Specifically, the theorem says that the sum of `f i j` over all pairs `(i, j)` such that `a ≤ i ≤ j < b` is the same whether we first fix `i` and sum over `j`, or first fix `j` and sum over `i`. The term `Finset.Ico a b` refers to the set of natural numbers starting from `a` and less than `b`.
More concisely: For any additive commutative monoid `M` and natural numbers `a < b`, the sum of a function `f : ℕ → ℕ → M` over `Finset.Ico a b` is the same whether summed over `i` first and then `j`, or summed over `j` first and then `i`.
|