List.prod_le_prod'
theorem List.prod_le_prod' :
∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {l : List ι} {f g : ι → M},
(∀ i ∈ l, f i ≤ g i) → (List.map f l).prod ≤ (List.map g l).prod
The theorem `List.prod_le_prod'` states that for all types `ι` and `M`, where `M` is a monoid and also has a preorder structure, if the multiplication operation in `M` is monotone when two factors are swapped and when they are not, then for any two functions `f` and `g` from `ι` to `M`, and any list `l` of type `ι`, if every element `i` in `l` satisfies the condition `f(i) ≤ g(i)`, then the product of the list resulting from mapping `f` over `l` is less than or equal to the product of the list resulting from mapping `g` over `l`. In simpler terms, the theorem states that if each output of `f` is less than or equal to the corresponding output of `g`, then the product of the outputs of `f` is less than or equal to the product of the outputs of `g`.
More concisely: If `M` is a monoid with a preorder structure and the multiplication operation is monotone, then for any functions `f` and `g` from a type `ι` to `M`, and any list `l` of type `ι` such that `f(i) ≤ g(i)` for all `i` in `l`, we have `prod (map f l) ≤ prod (map g l)`.
|
List.Sublist.sum_le_sum
theorem List.Sublist.sum_le_sum :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {l₁ l₂ : List M},
l₁.Sublist l₂ → (∀ a ∈ l₂, 0 ≤ a) → l₁.sum ≤ l₂.sum
This theorem states that if `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative, then the sum of the elements of `l₁` is less than or equal to the sum of the elements of `l₂`. This is stated for any type `M` that is an ordered monoid, i.e., it supports addition operation and a less than or equal to order that are compatible with each other. A stronger version of this theorem could be proven assuming that all the elements in the difference of `l₂` and `l₁` are nonnegative, but such a version is not yet in the `mathlib` library.
More concisely: If `l₁` is a sublist of nonnegative elements of `l₂` (an ordered monoid), then the sum of `l₁` is less than or equal to the sum of `l₂`.
|
List.Sublist.prod_le_prod'
theorem List.Sublist.prod_le_prod' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {l₁ l₂ : List M},
l₁.Sublist l₂ → (∀ a ∈ l₂, 1 ≤ a) → l₁.prod ≤ l₂.prod
The theorem `List.Sublist.prod_le_prod'` states that for any type `M` that forms a monoid and preorder, if list `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then the product of elements in `l₁` is less than or equal to the product of elements in `l₂`. The conditions in the theorem require the multiplication operation in `M` to respect the preorder relation, both when multiplying on the left and on the right. This theorem could be strengthened by assuming that all elements in the difference of `l₂` and `l₁` are greater than or equal to one, but such a version is not currently in `mathlib`.
More concisely: If `l₁` is a sublist of `l₂` consisting of elements greater than or equal to one from a monoid and preorder type `M` where multiplication respects the preorder relation, then `∏ l₁ ≤ ∏ l₂`.
|
List.monotone_sum_take
theorem List.monotone_sum_take :
∀ {M : Type u_3} [inst : CanonicallyOrderedAddCommMonoid M] (L : List M), Monotone fun i => (List.take i L).sum
The theorem `List.monotone_sum_take` states that for any type `M` which is a canonically ordered additive commutative monoid, and for any list `L` of type `M`, the function that takes an integer `i` and returns the sum of the first `i` elements of `L` (using the function `List.take`) is monotone. In other words, if `i` and `j` are integers such that `i` is less than or equal to `j`, then the sum of the first `i` elements of `L` is less than or equal to the sum of the first `j` elements of `L`. This is a formal way of saying that if you take more terms from the beginning of a list and sum them, you will get a number that is greater or equal to the sum of a lesser number of terms.
More concisely: For any additive commutative monoid M with a canonical order and any list L of length n in M, the function summing the first i elements of L is monotone, i.e., the sum of the first i elements is less than or equal to the sum of the first j elements for all i ≤ j.
|
List.sum_le_sum
theorem List.sum_le_sum :
∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {l : List ι} {f g : ι → M},
(∀ i ∈ l, f i ≤ g i) → (List.map f l).sum ≤ (List.map g l).sum
This theorem, `List.sum_le_sum`, states that given any types `ι` and `M`, where `M` is a monoid under addition and is also a preorder, and also satisfies covariant classes with respect to addition operation and less than or equal to relation, for any list `l` of elements of type `ι` and any two functions `f` and `g` from `ι` to `M`, if each element of the list `l` when mapped through function `f` is less than or equal to the same element when mapped through function `g`, then the sum of all the elements of list `l` when mapped through function `f` is less than or equal to the sum of all the elements when mapped through function `g`. In other words, if `f(i) ≤ g(i)` for all `i` in list `l`, then the sum of `f(i)` for all `i` in `l` is less than or equal to the sum of `g(i)` for all `i` in `l`.
More concisely: Given a list `l` of elements from a preorder `(ι, ≤)` with monoid structure `M` under addition, if `f(i) ≤ g(i)` for all `i` in `l`, then `Σ(i in l) f i ≤ Σ(i in l) g i`.
|