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.

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

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.

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)

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)

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

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|

@[simp]

theorem Finset.PNat.coe_prod {ι : Type u_4} (f : ι → ℕ+) (s : Finset ι) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

@[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.

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

theorem Finset.sum_sq_le_sum_mul_sum_of_sq_le_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 usually 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.

@[deprecated Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul (since := "2026-05-12")]

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

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.

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

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)

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)

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)

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

theorem Mathlib.Meta.Positivity.prod_ne_zero {ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀] [NoZeroDivisors M₀] : (∀ a ∈ s, f a ≠ 0) → ∏ x ∈ s, f x ≠ 0

Alias of the reverse direction of Finset.prod_ne_zero_iff.

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.