Documentation

Mathlib.Algebra.Order.BigOperators.Ring.Finset

Big operators on a finset in ordered rings #

This file contains the results concerning the interaction of finset big operators with ordered rings.

theorem Finset.prod_nonneg {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f : ιR} {s : Finset ι} (h0 : is, 0 f i) :
0 is, f i
theorem Finset.prod_le_prod {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f : ιR} {g : ιR} {s : Finset ι} (h0 : is, 0 f i) (h1 : is, f i g i) :
is, f i is, g i

If all f i, i ∈ s, are nonnegative and each f i is less than or equal to g i, then the product of f i is less than or equal to the product of g i. See also Finset.prod_le_prod' for the case of an ordered commutative multiplicative monoid.

theorem GCongr.prod_le_prod {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f : ιR} {g : ιR} {s : Finset ι} (h0 : is, 0 f i) (h1 : is, f i g i) :
s.prod f s.prod g

If all f i, i ∈ s, are nonnegative and each f i is less than or equal to g i, then the product of f i is less than or equal to the product of g i.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_le_prod, convenient for the gcongr tactic.

theorem Finset.prod_le_one {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f : ιR} {s : Finset ι} (h0 : is, 0 f i) (h1 : is, f i 1) :
is, f i 1

If each f i, i ∈ s belongs to [0, 1], then their product is less than or equal to one. See also Finset.prod_le_one' for the case of an ordered commutative multiplicative monoid.

theorem Finset.prod_pos {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f : ιR} {s : Finset ι} (h0 : is, 0 < f i) :
0 < is, f i
theorem Finset.prod_lt_prod {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f : ιR} {g : ιR} {s : Finset ι} (hf : is, 0 < f i) (hfg : is, f i g i) (hlt : is, f i < g i) :
is, f i < is, g i
theorem Finset.prod_lt_prod_of_nonempty {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f : ιR} {g : ιR} {s : Finset ι} (hf : is, 0 < f i) (hfg : is, f i < g i) (h_ne : s.Nonempty) :
is, f i < is, g i
theorem Finset.prod_add_prod_le {ι : Type u_1} {R : Type u_2} [OrderedCommSemiring R] {s : Finset ι} {i : ι} {f : ιR} {g : ιR} {h : ιR} (hi : i s) (h2i : g i + h i f i) (hgf : js, j ig j f j) (hhf : js, j ih j f j) (hg : is, 0 g i) (hh : is, 0 h i) :
is, g i + is, h i is, f i

If g, h ≤ f and g i + h i ≤ f i, then the product of f over s is at least the sum of the products of g and h. This is the version for OrderedCommSemiring.

theorem Finset.sum_mul_sq_le_sq_mul_sq {ι : Type u_1} {R : Type u_2} [LinearOrderedCommSemiring R] [ExistsAddOfLE R] (s : Finset ι) (f : ιR) (g : ιR) :
(is, f i * g i) ^ 2 (is, f i ^ 2) * is, g i ^ 2

Cauchy-Schwarz inequality for finsets.

theorem Finset.abs_prod {ι : Type u_1} {R : Type u_2} [LinearOrderedCommRing R] (s : Finset ι) (f : ιR) :
|xs, f x| = xs, |f x|
@[simp]
theorem CanonicallyOrderedCommSemiring.prod_pos {ι : Type u_1} {R : Type u_2} [CanonicallyOrderedCommSemiring R] {f : ιR} {s : Finset ι} [Nontrivial R] :
0 < is, f i is, 0 < f i

Note that the name is to match CanonicallyOrderedCommSemiring.mul_pos.

theorem Finset.prod_add_prod_le' {ι : Type u_1} {R : Type u_2} [CanonicallyOrderedCommSemiring R] {f : ιR} {g : ιR} {h : ιR} {s : Finset ι} {i : ι} (hi : i s) (h2i : g i + h i f i) (hgf : js, j ig j f j) (hhf : js, j ih j f j) :
is, g i + is, h i is, f i

If g, h ≤ f and g i + h i ≤ f i, then the product of f over s is at least the sum of the products of g and h. This is the version for CanonicallyOrderedCommSemiring.

theorem AbsoluteValue.sum_le {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) (s : Finset ι) (f : ιR) :
abv (is, f i) is, abv (f i)
theorem IsAbsoluteValue.abv_sum {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [OrderedSemiring S] (abv : RS) [IsAbsoluteValue abv] (f : ιR) (s : Finset ι) :
abv (is, f i) is, abv (f i)
@[deprecated IsAbsoluteValue.abv_sum]
theorem abv_sum_le_sum_abv {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [OrderedSemiring S] (abv : RS) [IsAbsoluteValue abv] (f : ιR) (s : Finset ι) :
abv (is, f i) is, abv (f i)

Alias of IsAbsoluteValue.abv_sum.

theorem AbsoluteValue.map_prod {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S] (abv : AbsoluteValue R S) (f : ιR) (s : Finset ι) :
abv (is, f i) = is, abv (f i)
theorem IsAbsoluteValue.map_prod {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S] (abv : RS) [IsAbsoluteValue abv] (f : ιR) (s : Finset ι) :
abv (is, f i) = is, abv (f i)

The positivity extension which proves that ∏ i ∈ s, f i is nonnegative if f is, and positive if each f i is.

TODO: The following example does not work

example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.prod f := by positivity

because compareHyp can't look for assumptions behind binders.

Instances For