Finset.prod_le_prod
theorem Finset.prod_le_prod :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [inst_2 : ZeroLEOneClass R]
[inst_3 : PosMulMono R] {f g : ι → R} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → (s.prod fun i => f i) ≤ s.prod fun i => g i
The theorem `Finset.prod_le_prod` states that for a given set `s` of type `ι` and two functions `f, g: ι → R` where `R` is a commutative monoid with zero, a partial order, and where multiplication is monotonic for nonnegative elements, if all elements `f i` for `i ∈ s` are nonnegative, and each `f i` is less than or equal to `g i`, then the total product of `f i` over all `i` in `s` is less than or equal to the total product of `g i` over all `i` in `s`. This theorem is also applicable to an ordered commutative multiplicative monoid.
More concisely: Given a commutative monoid with zero, partial order, and monotonic multiplication for nonnegative elements `R`, and functions `f, g: ι → R` with nonnegative and `≤`-related images on a set `s`, the total product of `f i` over `i ∈ s` is less than or equal to the total product of `g i` over `i ∈ s`.
|
Finset.prod_pos
theorem Finset.prod_pos :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [inst_2 : ZeroLEOneClass R]
[inst_3 : PosMulStrictMono R] [inst_4 : Nontrivial R] {f : ι → R} {s : Finset ι},
(∀ i ∈ s, 0 < f i) → 0 < s.prod fun i => f i
The theorem `Finset.prod_pos` states that for any type `ι` and any type `R` such that `R` forms a commutative monoid with zero, has a partial order, satisfies the zero less than or equal to one class property, has a strict monotonicity of multiplication by positive elements on the left, and is nontrivial, if you have a function `f` from `ι` to `R` and a finite set `s` of type `ι`, then if all elements `i` in `s` have the property that `f(i)` is greater than zero, the product of `f(i)` over all `i` in `s` is also greater than zero. In other words, the positive product of positive elements in a finite set is also positive.
More concisely: For any commutative monoid with zero, partial order, zero less than or equal to one property, strict monotonicity of multiplication by positive elements on the left, and nontriviality, if `f : ι -> R` maps a finite set `s ⊆ ι` to positive elements, then `∏ (i ∈ s) f(i) > 0`.
|
Finset.prod_nonneg
theorem Finset.prod_nonneg :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [inst_2 : ZeroLEOneClass R]
[inst_3 : PosMulMono R] {f : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → 0 ≤ s.prod fun i => f i
The theorem `Finset.prod_nonneg` asserts that for any type `ι`, any commutative monoid `R` with zero that also has partial order and satisfies the `ZeroLEOneClass` and `PosMulMono` properties, any function `f` from `ι` to `R`, and any finite set `s` of type `ι`, if every element `i` of `s` satisfies `0 ≤ f i`, then the product of `f i` over all `i` in `s` is also nonnegative, i.e., `0 ≤ Finset.prod s fun i => f i`. Essentially, it states that the product of nonnegative numbers on a given finite set is also nonnegative.
More concisely: If `R` is a commutative monoid with zero, partial order, and `ZeroLEOneClass` and `PosMulMono` properties, and `f : ι -> R` maps a finite set `s` of nonnegative elements `i` in `ι`, then the product `Finset.prod s fun i => f i` is nonnegative.
|
Finset.prod_add_prod_le
theorem Finset.prod_add_prod_le :
∀ {ι : Type u_1} {R : Type u_2} [inst : OrderedCommSemiring R] {s : Finset ι} {i : ι} {f g h : ι → R},
i ∈ s →
g i + h i ≤ f i →
(∀ j ∈ s, j ≠ i → g j ≤ f j) →
(∀ j ∈ s, j ≠ i → h j ≤ f j) →
(∀ i ∈ s, 0 ≤ g i) →
(∀ i ∈ s, 0 ≤ h i) → ((s.prod fun i => g i) + s.prod fun i => h i) ≤ s.prod fun i => f i
The theorem `Finset.prod_add_prod_le` states that for any set `s` of type `ι`, any element `i` in `s`, and any three functions `f`, `g`, and `h` from `ι` to `R` (where `R` is an ordered commutative semiring), if `g i + h i` is less than or equal to `f i` and `g j` and `h j` are less than or equal to `f j` for all `j` in `s` (where `j` is not equal to `i`), and if all values of `g i` and `h i` are greater than or equal to zero for all `i` in `s`, then the sum of the products of `g` and `h` over `s` is less than or equal to the product of `f` over `s`.
More concisely: For any set `s`, function `f, g, h` from `s` to an ordered commutative semiring `R` with `g(i)`, `h(i)` > 0 for all `i` in `s`, and `g(i) + h(i) ≤ f(i)` for all `i` in `s` and `g(j) ≤ f(j)`, `h(j) ≤ f(j)` for all `j` in `s` with `j ≠ i`, the product of `g` and `h` over `s` is less than or equal to the product of `f` over `s`.
|
Finset.prod_le_one
theorem Finset.prod_le_one :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [inst_2 : ZeroLEOneClass R]
[inst_3 : PosMulMono R] {f : ι → R} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ 1) → (s.prod fun i => f i) ≤ 1
The theorem `Finset.prod_le_one` states that if we have a finite set `s` of elements of type `ι`, and a function `f : ι → R` mapping these elements into a commutative monoid with zero `R` endowed with a partial order and the property that multiplication by nonnegative elements is monotone, then if each `f i` for `i ∈ s` lies in the interval `[0, 1]`, the product of these `f i` over all `i ∈ s` is less than or equal to one. This is a generalization that also applies to structures that are not necessarily ordered commutative multiplicative monoids.
More concisely: If `s` is a finite set of elements from a commutative monoid `R` with zero and a monotone multiplication by nonnegative elements, and each `f(i)` in the image of the function `f : ι → R` lies in the interval `[0, 1]`, then the product of `f i` for all `i ∈ s` is less than or equal to one.
|
GCongr.prod_le_prod
theorem GCongr.prod_le_prod :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [inst_2 : ZeroLEOneClass R]
[inst_3 : PosMulMono R] {f g : ι → R} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → s.prod f ≤ s.prod g
The theorem `GCongr.prod_le_prod` asserts that for any index set `ι`, any type `R` that is a commutative monoid with zero, has a partial order, has a `ZeroLEOneClass` and a `PosMulMono` property, any two functions `f` and `g` from `ι` to `R`, and any finite set `s` of indices from `ι`, if all the values `f i` for `i` in `s` are nonnegative and each `f i` is less than or equal to `g i`, then the product of the `f i` over all `i` in `s` is less than or equal to the product of the `g i` over all `i` in `s`. This is a more specific, beta-reduced version of the standard lemma `Finset.prod_le_prod`, designed to be convenient for use with the `gcongr` tactic.
More concisely: For any commutative monoid with zero, partial order, and `ZeroLEOneClass` and `PosMulMono` properties, if two functions from an index set to the monoid have the same values at finitely many indices and all values are nonnegative with the function from the first set being less than or equal to the function from the second set at those indices, then the product of the values from the first function is less than or equal to the product of the values from the second function.
|
AbsoluteValue.sum_le
theorem AbsoluteValue.sum_le :
∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : OrderedSemiring S]
(abv : AbsoluteValue R S) (s : Finset ι) (f : ι → R), abv (s.sum fun i => f i) ≤ s.sum fun i => abv (f i)
The theorem `AbsoluteValue.sum_le` states that for any semiring `R`, ordered semiring `S`, absolute value function `abv : AbsoluteValue R S`, finite set `s : Finset ι`, and function `f : ι → R`, the absolute value of the sum of `f i` as `i` ranges over the elements of the finite set `s` is less than or equal to the sum of the absolute values of `f i` over the same set `s`. In math terms, it says that for any absolute value and any finite sum, the absolute value of the sum is less than or equal to the sum of the absolute values. This captures the idea of the triangle inequality for finite sums.
More concisely: For any semiring `R` with absolute value function `abv`, ordered semiring `S`, finite set `s`, and function `f : ι → R`, the absolute value of the sum of `f i` over `s` is less than or equal to the sum of the absolute values of `f i` over `s`. (In mathematical notation: `∫in s abv (∑i in s f i) ≤ ∑i in s abv (fi)`)
|
CanonicallyOrderedCommSemiring.prod_pos
theorem CanonicallyOrderedCommSemiring.prod_pos :
∀ {ι : Type u_1} {R : Type u_2} [inst : CanonicallyOrderedCommSemiring R] {f : ι → R} {s : Finset ι}
[inst_1 : Nontrivial R], (0 < s.prod fun i => f i) ↔ ∀ i ∈ s, 0 < f i
This theorem, `CanonicallyOrderedCommSemiring.prod_pos`, states that for any type `ι`, any canonically ordered commutative semiring `R`, and any function `f` from `ι` to `R`, the product of the function values over a finite set `s` of `ι` is greater than zero if and only if every function value for each element in `s` is greater than zero. This holds true as long as `R` is nontrivial (i.e., it has at least two distinct elements).
More concisely: Given a finite non-empty set `s` and a function `f` from a type `ι` to a nontrivial canonically ordered commutative semiring `R`, the product of `f` over `s` is positive if and only if every value `f(i)` for `i` in `s` is positive.
|
Finset.prod_add_prod_le'
theorem Finset.prod_add_prod_le' :
∀ {ι : Type u_1} {R : Type u_2} [inst : CanonicallyOrderedCommSemiring R] {f g h : ι → R} {s : Finset ι} {i : ι},
i ∈ s →
g i + h i ≤ f i →
(∀ j ∈ s, j ≠ i → g j ≤ f j) →
(∀ j ∈ s, j ≠ i → h j ≤ f j) → ((s.prod fun i => g i) + s.prod fun i => h i) ≤ s.prod fun i => f i
This theorem states that for a certain type of mathematical structure known as a `CanonicallyOrderedCommSemiring`, if a function `f` is greater than or equal to two other functions `g` and `h` at every point in a finite set `s`, and the sum of `g` and `h` at any point `i` in `s` is also less than or equal to `f` at that point, then the total product of the values of `f` over `s` is greater than or equal to the sum of the separate products of the values of `g` and `h` over `s`. The theorem is precise in its conditions - it requires that `f` dominates `g` and `h` everywhere in `s` except possibly at the specific point `i`.
More concisely: For a `CanonicallyOrderedCommSemiring` `s` and functions `f ≥ g, h: s → s` such that `g(i) + h(i) ≤ f(i)` for all `i` in a finite set `S` except possibly at one point, we have `∏(f(i): i ∈ S) ≥ ∏(g(i): i ∈ S) * ∏(h(i): i ∈ S)`.
|