# Big operators on a finset in ordered rings #

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

In particular, this file contains the standard form of the Cauchy-Schwarz inequality, as well as some of its immediate consequences.

source
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 ≤ ∏ i ∈ s, f i
source
theorem Finset.prod_le_prod {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f g : ι → R} {s : Finset ι} (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
∏ i ∈ s, f i ≤ ∏ i ∈ s, 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.

source
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) :
∏ i ∈ s, 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.

source
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 < ∏ i ∈ s, f i
source
theorem Finset.prod_lt_prod {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι} (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i
source
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 g : ι → R} {s : Finset ι} (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i) (h_ne : s.Nonempty) :
∏ i ∈ s, f i < ∏ i ∈ s, g i
source
theorem Finset.sum_sq_le_sq_sum_of_nonneg {ι : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] {f : ι → R} {s : Finset ι} (hf : ∀ i ∈ s, 0 ≤ f i) :
∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2
source
theorem Finset.prod_add_prod_le {ι : Type u_1} {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset ι} {i : ι} {f g 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) :
∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, 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`.

source
theorem Finset.le_prod_of_submultiplicative_on_pred_of_nonneg {ι : Type u_1} {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {M : Type u_4} [CommMonoid M] (f : M → R) (p : M → Prop) (h_nonneg : ∀ (a : M), 0 ≤ f a) (h_one : f 1 ≤ 1) (h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ (a b : M), p a → p b → p (a * b)) (s : Finset ι) (g : ι → M) (hps : ∀ a ∈ s, p (g a)) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
source
theorem Finset.le_prod_of_submultiplicative_of_nonneg {ι : Type u_1} {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {M : Type u_4} [CommMonoid M] (f : M → R) (h_nonneg : ∀ (a : M), 0 ≤ f a) (h_one : f 1 ≤ 1) (h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
source
theorem Finset.sum_mul_self_eq_zero_iff {ι : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι) (f : ι → R) :
∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0
source
theorem Finset.abs_prod {ι : Type u_1} {R : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι) (f : ι → R) :
|∏ x ∈ s, f x| = ∏ x ∈ s, |f x|
source
@[simp]
theorem Finset.PNat.coe_prod {ι : Type u_4} (f : ι → ℕ+) (s : Finset ι) :
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
source
@[simp]
theorem CanonicallyOrderedAdd.prod_pos {ι : Type u_1} {R : Type u_2} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] {f : ι → R} {s : Finset ι} [NoZeroDivisors R] [Nontrivial R] :
0 < ∏ i ∈ s, f i ↔ ∀ i ∈ s, 0 < f i

Note that the name is to match `CanonicallyOrderedAdd.mul_pos`.

source
theorem Finset.prod_add_prod_le' {ι : Type u_1} {R : Type u_2} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] {f g 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) :
∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, 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 `CanonicallyOrderedAdd`.

### Named inequalities #

source
theorem Finset.sum_sq_le_sum_mul_sum_of_sq_eq_mul {ι : Type u_1} {R : Type u_2} [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι) {r f g : ι → R} (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) (ht : ∀ i ∈ s, r i ^ 2 = f i * g i) :
(∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Cauchy-Schwarz inequality for finsets.

This is written in terms of sequences `f`, `g`, and `r`, where `r` is a stand-in for `√(f i * g i)`. See `sum_mul_sq_le_sq_mul_sq` for the more usual form in terms of squared sequences.

source
theorem Finset.sum_mul_sq_le_sq_mul_sq {ι : Type u_1} {R : Type u_2} [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι) (f g : ι → R) :
(∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2

Cauchy-Schwarz inequality for finsets, squared version.

source
theorem Finset.sq_sum_div_le_sum_sq_div {ι : Type u_1} {R : Type u_2} [Semifield R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι) (f : ι → R) {g : ι → R} (hg : ∀ i ∈ s, 0 < g i) :
(∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Sedrakyan's lemma, aka Titu's lemma or Engel's form.

This is a specialization of the Cauchy-Schwarz inequality with the sequences `f n / √(g n)` and `√(g n)`, though here it is proven without relying on square roots.

### Absolute values #

source
theorem AbsoluteValue.sum_le {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S] (abv : AbsoluteValue R S) (s : Finset ι) (f : ι → R) :
abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)
source
theorem IsAbsoluteValue.abv_sum {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) :
abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)
source
theorem AbsoluteValue.map_prod {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι) :
abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)
source
theorem IsAbsoluteValue.map_prod {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) :
abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)

### Positivity extension #

source
def Mathlib.Meta.Positivity.evalFinsetProd :
PositivityExt

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