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 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ Finset.prod s fun (i : ι) => 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 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : (Finset.prod s fun (i : ι) => f i) ≤ Finset.prod s fun (i : ι) => 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 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : Finset.prod s f ≤ Finset.prod s 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 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : (Finset.prod s fun (i : ι) => 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 : ∀ i ∈ s, 0 < f i) : 0 < Finset.prod s fun (i : ι) => 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 : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => 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 : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i) (h_ne : s.Nonempty) : (Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => 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 : ∀ j ∈ s, j ≠ i → g j ≤ f j) (hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) (hg : ∀ i ∈ s, 0 ≤ g i) (hh : ∀ i ∈ s, 0 ≤ h i) : ((Finset.prod s fun (i : ι) => g i) + Finset.prod s fun (i : ι) => h i) ≤ Finset.prod s fun (i : ι) => 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) : (Finset.sum s fun (i : ι) => f i * g i) ^ 2 ≤ (Finset.sum s fun (i : ι) => f i ^ 2) * Finset.sum s fun (i : ι) => 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) : |Finset.prod s fun (x : ι) => f x| = Finset.prod s fun (x : ι) => |f x|

@[simp]

theorem CanonicallyOrderedCommSemiring.prod_pos {ι : Type u_1} {R : Type u_2} [CanonicallyOrderedCommSemiring R] {f : ι → R} {s : Finset ι} [Nontrivial R] : (0 < Finset.prod s fun (i : ι) => f i) ↔ ∀ i ∈ s, 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 : ∀ j ∈ s, j ≠ i → g j ≤ f j) (hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) : ((Finset.prod s fun (i : ι) => g i) + Finset.prod s fun (i : ι) => h i) ≤ Finset.prod s fun (i : ι) => 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 (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => abv (f i)

theorem IsAbsoluteValue.abv_sum {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [OrderedSemiring S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) : abv (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => 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 : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) : abv (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => 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 (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => 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 : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) : abv (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => abv (f i)