Mathlib.Algebra.Order.BigOperators.Ring.Finset

Finset.prod_nonneg theorem

(h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i

Full source

lemma prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i :=
  prod_induction f (fun i ↦ 0 ≤ i) (fun _ _ ha hb ↦ mul_nonneg ha hb) zero_le_one h0

Nonnegativity of Finite Product with Nonnegative Factors

Informal description

For any finite set $s$ and any function $f$ defined on $s$, if $f(i) \geq 0$ for all $i \in s$, then the product $\prod_{i \in s} f(i)$ is nonnegative.

Finset.prod_le_prod theorem

(h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Full source

/-- 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. -/
@[gcongr]
lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
    ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    gcongr
    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

Monotonicity of Finite Product under Nonnegative Pointwise Inequality

Informal description

For any finite set $s$ and functions $f, g$ defined on $s$, if $0 \leq f(i) \leq g(i)$ for all $i \in s$, then the product $\prod_{i \in s} f(i)$ is less than or equal to the product $\prod_{i \in s} g(i)$.

Finset.prod_le_one theorem

(h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1

Full source

/-- 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. -/
lemma prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 := by
  convert ← prod_le_prod h0 h1
  exact Finset.prod_const_one

Finite Product Bound for Functions in $[0,1]$

Informal description

For any finite set $s$ and any function $f$ defined on $s$, if $0 \leq f(i) \leq 1$ for all $i \in s$, then the product $\prod_{i \in s} f(i)$ is less than or equal to $1$.

Finset.prod_pos theorem

(h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i

Full source

lemma prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i :=
  prod_induction f (fun x ↦ 0 < x) (fun _ _ ha hb ↦ mul_pos ha hb) zero_lt_one h0

Positivity of Finite Product of Positive Elements

Informal description

For any finite set $s$ and any function $f$ such that $f(i) > 0$ for all $i \in s$, the product $\prod_{i \in s} f(i)$ is strictly positive.

Finset.prod_lt_prod theorem

 (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

Full source

lemma prod_lt_prod (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 := by
  classical
  obtain ⟨i, hi, hilt⟩ := hlt
  rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
  · exact (hf i hi).le.trans hilt.le

Strict Monotonicity of Finite Product under Pointwise Inequality with Positive Elements

Informal description

Let $s$ be a finite set and let $f, g$ be functions defined on $s$ such that: 1. $f(i) > 0$ for all $i \in s$, 2. $f(i) \leq g(i)$ for all $i \in s$, 3. There exists some $j \in s$ such that $f(j) < g(j)$. Then the product of $f$ over $s$ is strictly less than the product of $g$ over $s$, i.e., \[ \prod_{i \in s} f(i) < \prod_{i \in s} g(i). \]

Finset.prod_lt_prod_of_nonempty theorem

(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

Full source

lemma prod_lt_prod_of_nonempty (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 := by
  apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)
  obtain ⟨i, hi⟩ := h_ne
  exact ⟨i, hi, hfg i hi⟩

Strict Monotonicity of Finite Product under Strict Pointwise Inequality with Positive Elements

Informal description

Let $s$ be a nonempty finite set and let $f, g$ be functions defined on $s$ such that: 1. $f(i) > 0$ for all $i \in s$, 2. $f(i) < g(i)$ for all $i \in s$. Then the product of $f$ over $s$ is strictly less than the product of $g$ over $s$, i.e., \[ \prod_{i \in s} f(i) < \prod_{i \in s} g(i). \]

Finset.sum_sq_le_sq_sum_of_nonneg theorem

(hf : ∀ i ∈ s, 0 ≤ f i) : ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2

Full source

lemma sum_sq_le_sq_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) :
    ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2 := by
  simp only [sq, sum_mul_sum]
  refine sum_le_sum fun i hi ↦ ?_
  rw [← mul_sum]
  gcongr
  · exact hf i hi
  · exact single_le_sum hf hi

Sum of Squares Inequality for Nonnegative Functions

Informal description

For any finite set $s$ and any nonnegative real-valued function $f$ defined on $s$ (i.e., $f(i) \geq 0$ for all $i \in s$), the sum of squares of $f$ is less than or equal to the square of the sum of $f$: \[ \sum_{i \in s} f(i)^2 \leq \left(\sum_{i \in s} f(i)\right)^2. \]

Finset.prod_add_prod_le theorem

 {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

Full source

/-- 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`. -/
lemma prod_add_prod_le {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 := by
  classical
  simp_rw [prod_eq_mul_prod_diff_singleton hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

Sum of Products Inequality for Ordered Semirings

Informal description

Let $s$ be a finite set, $R$ an ordered commutative semiring, and $f, g, h : s \to R$ functions such that: 1. There exists an element $i \in s$ where $g(i) + h(i) \leq f(i)$, 2. For all $j \in s$ with $j \neq i$, we have $g(j) \leq f(j)$ and $h(j) \leq f(j)$, 3. All values of $g$ and $h$ are nonnegative on $s$. Then the sum of the products of $g$ and $h$ over $s$ is bounded by the product of $f$ over $s$: \[ \left(\prod_{i \in s} g(i)\right) + \left(\prod_{i \in s} h(i)\right) \leq \prod_{i \in s} f(i). \]

Finset.le_prod_of_submultiplicative_on_pred_of_nonneg theorem

 {M : Type*} [CommMonoid M] (f : M → R) (p : M → Prop) (h_nonneg : ∀ a, 0 ≤ f a) (h_one : f 1 ≤ 1)
  (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b)) (s : Finset ι) (g : ι → M)
  (hps : ∀ a, a ∈ s → p (g a)) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Full source

theorem le_prod_of_submultiplicative_on_pred_of_nonneg {M : Type*} [CommMonoid M] (f : M → R)
    (p : M → Prop) (h_nonneg : ∀ a, 0 ≤ f a) (h_one : f 1 ≤ 1)
    (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
    (s : Finset ι) (g : ι → M) (hps : ∀ a, a ∈ s → p (g a)) :
    f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) := by
  apply le_trans (Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg f p h_nonneg h_one
    h_mul hp_mul _ ?_) (by simp [Multiset.map_map])
  intro _ ha
  obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp ha
  exact hps i hi

Submultiplicative Inequality for Predicate-Restricted Functions on Finite Products

Informal description

Let $M$ be a commutative monoid and $R$ be an ordered ring. Given a function $f : M \to R$ and a predicate $p : M \to \text{Prop}$ satisfying: 1. Nonnegativity: $f(a) \geq 0$ for all $a \in M$, 2. Submultiplicativity on $p$: $f(a \cdot b) \leq f(a) \cdot f(b)$ for all $a, b \in M$ with $p(a)$ and $p(b)$, 3. Predicate closure: $p(a \cdot b)$ holds whenever $p(a)$ and $p(b)$ hold, 4. Unit condition: $f(1) \leq 1$, then for any finite set $s$ and function $g : s \to M$ such that $p(g(i))$ holds for all $i \in s$, we have \[ f\left(\prod_{i \in s} g(i)\right) \leq \prod_{i \in s} f(g(i)). \]

Finset.le_prod_of_submultiplicative_of_nonneg theorem

 {M : Type*} [CommMonoid M] (f : M → R) (h_nonneg : ∀ a, 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)

Full source

theorem le_prod_of_submultiplicative_of_nonneg {M : Type*} [CommMonoid M]
    (f : M → R) (h_nonneg : ∀ a, 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) :=
  le_trans (Multiset.le_prod_of_submultiplicative_of_nonneg f h_nonneg h_one h_mul _)
    (by simp [Multiset.map_map])

Submultiplicative Inequality for Finite Products in Ordered Rings

Informal description

Let $M$ be a commutative monoid and $R$ an ordered ring. Given a function $f : M \to R$ satisfying: 1. Nonnegativity: $f(a) \geq 0$ for all $a \in M$, 2. Submultiplicativity: $f(x \cdot y) \leq f(x) \cdot f(y)$ for all $x, y \in M$, 3. Unit condition: $f(1) \leq 1$, then for any finite set $s$ and function $g : s \to M$, we have \[ f\left(\prod_{i \in s} g(i)\right) \leq \prod_{i \in s} f(g(i)). \]

Finset.sum_mul_self_eq_zero_iff theorem

 [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι) (f : ι → R) :
  ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0

Full source

theorem sum_mul_self_eq_zero_iff [Semiring R] [LinearOrder R] [IsStrictOrderedRing R]
    [ExistsAddOfLE R] (s : Finset ι)
    (f : ι → R) : ∑ i ∈ s, f i * f i∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
  rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]
  simp

Sum of Squares Vanishes if and only if All Terms Vanish in Strictly Ordered Rings

Informal description

Let $R$ be a semiring with a linear order and a strictly ordered ring structure, and assume that for any two elements $a, b \in R$ with $a \leq b$, there exists an element $c \in R$ such that $a + c = b$. For any finite set $s$ and function $f : s \to R$, the sum of squares $\sum_{i \in s} f(i)^2$ is zero if and only if $f(i) = 0$ for all $i \in s$.

Finset.abs_prod theorem

 [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι) (f : ι → R) : |∏ x ∈ s, f x| = ∏ x ∈ s, |f x|

Full source

lemma abs_prod [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι) (f : ι → R) :
    |∏ x ∈ s, f x| = ∏ x ∈ s, |f x| :=
  map_prod absHom _ _

Absolute Value of Finite Product Equals Product of Absolute Values in Ordered Rings

Informal description

Let $R$ be a commutative ring with a linear order and a strictly ordered ring structure. For any finite set $s$ and function $f : s \to R$, the absolute value of the product $\prod_{x \in s} f(x)$ is equal to the product of the absolute values $\prod_{x \in s} |f(x)|$.

Finset.PNat.coe_prod theorem

{ι : Type*} (f : ι → ℕ+) (s : Finset ι) : ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : ℕ)

Full source

@[simp, norm_cast]
theorem PNat.coe_prod {ι : Type*} (f : ι → ℕ+) (s : Finset ι) :
    ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : ℕ) :=
  map_prod PNat.coeMonoidHom _ _

Canonical Map Commutes with Finite Product of Positive Natural Numbers

Informal description

For any finite set $s$ and any function $f$ from $s$ to the positive natural numbers $\mathbb{N}^+$, the canonical map from positive natural numbers to natural numbers commutes with the product operation. That is, the image of the product $\prod_{i \in s} f(i)$ under this map equals the product $\prod_{i \in s} f(i)$ computed in $\mathbb{N}$.

CanonicallyOrderedAdd.prod_pos theorem

[NoZeroDivisors R] [Nontrivial R] : 0 < ∏ i ∈ s, f i ↔ (∀ i ∈ s, (0 : R) < f i)

Full source

/-- Note that the name is to match `CanonicallyOrderedAdd.mul_pos`. -/
@[simp] lemma _root_.CanonicallyOrderedAdd.prod_pos [NoZeroDivisors R] [Nontrivial R] :
    0 < ∏ i ∈ s, f i ↔ (∀ i ∈ s, (0 : R) < f i) :=
  CanonicallyOrderedAdd.multiset_prod_pos.trans Multiset.forall_mem_map_iff

Positivity of Finite Product in Ordered Ring

Informal description

Let $R$ be a nontrivial ordered ring with no zero divisors, and let $s$ be a finite set. For a function $f : s \to R$, the product $\prod_{i \in s} f(i)$ is positive if and only if $f(i) > 0$ for every $i \in s$.

Finset.prod_add_prod_le' theorem

 (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

Full source

/-- 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`.
-/
lemma prod_add_prod_le' (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 := by
  classical
  simp_rw [prod_eq_mul_prod_diff_singleton hi]
  refine le_trans ?_ (mul_le_mul_right' h2i _)
  rw [right_distrib]
  gcongr with j hj j hj <;> simp_all

Product Sum Inequality in Canonically Ordered Monoids: $\prod g + \prod h \leq \prod f$ under pointwise bounds

Informal description

Let $s$ be a finite set and $f, g, h$ be functions from $s$ to a canonically ordered additive monoid $\alpha$. Suppose there exists an element $i \in s$ such that: 1. $g(i) + h(i) \leq f(i)$, and 2. For all $j \in s$ with $j \neq i$, both $g(j) \leq f(j)$ and $h(j) \leq f(j)$ hold. Then the sum of the products $\prod_{i \in s} g(i) + \prod_{i \in s} h(i)$ is less than or equal to the product $\prod_{i \in s} f(i)$.

Finset.sum_sq_le_sum_mul_sum_of_sq_eq_mul theorem

 [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

Full source

/-- **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. -/
lemma sum_sq_le_sum_mul_sum_of_sq_eq_mul [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 := by
  obtain h | h := (sum_nonneg hg).eq_or_gt
  · have ht' : ∑ i ∈ s, r i = 0 := sum_eq_zero fun i hi ↦ by
      simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi
    rw [h, ht']
    simp
  · refine le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h
    calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 =
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            conv_rhs => rw [mul_mul_mul_comm, ← ht i hi]
            ring
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_eq_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring

Cauchy-Schwarz Inequality for Finite Sums with Squared Product Condition

Informal description

Let $R$ be a commutative semiring with a linear order and a strict ordered ring structure, and assume that for any two elements $a, b \in R$ with $a \leq b$, there exists an element $c \in R$ such that $a + c = b$. Let $s$ be a finite set, and let $r, f, g : s \to R$ be functions such that for every $i \in s$, $f(i) \geq 0$, $g(i) \geq 0$, and $r(i)^2 = f(i) \cdot g(i)$. Then, the following inequality holds: \[ \left( \sum_{i \in s} r(i) \right)^2 \leq \left( \sum_{i \in s} f(i) \right) \cdot \left( \sum_{i \in s} g(i) \right). \]

Finset.sum_mul_sq_le_sq_mul_sq theorem

 [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

Full source

/-- **Cauchy-Schwarz inequality** for finsets, squared version. -/
lemma sum_mul_sq_le_sq_mul_sq [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 :=
  sum_sq_le_sum_mul_sum_of_sq_eq_mul s
    (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ mul_pow ..)

Cauchy-Schwarz Inequality for Finite Sums: $(\sum f_i g_i)^2 \leq (\sum f_i^2)(\sum g_i^2)$

Informal description

Let $R$ be a commutative semiring with a linear order and a strict ordered ring structure, and assume that for any two elements $a, b \in R$ with $a \leq b$, there exists an element $c \in R$ such that $a + c = b$. Let $s$ be a finite set, and let $f, g : s \to R$ be arbitrary functions. Then the following inequality holds: \[ \left( \sum_{i \in s} f(i) g(i) \right)^2 \leq \left( \sum_{i \in s} f(i)^2 \right) \left( \sum_{i \in s} g(i)^2 \right). \]

Finset.sq_sum_div_le_sum_sq_div theorem

 [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

Full source

/-- **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. -/
theorem sq_sum_div_le_sum_sq_div [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 := by
  have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le
  have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)
  refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H)
    (sum_sq_le_sum_mul_sum_of_sq_eq_mul _ H hg' fun i hi ↦ ?_)
  rw [div_mul_cancel₀]
  exact (hg i hi).ne'

Sedrakyan's Lemma (Titu's Lemma) for Finite Sums: $\frac{(\sum f_i)^2}{\sum g_i} \leq \sum \frac{f_i^2}{g_i}$

Informal description

Let $R$ be a semifield with a linear order and a strict ordered ring structure, and assume that for any two elements $a, b \in R$ with $a \leq b$, there exists an element $c \in R$ such that $a + c = b$. Let $s$ be a finite set, and let $f, g : s \to R$ be functions such that $g(i) > 0$ for all $i \in s$. Then the following inequality holds: \[ \frac{\left( \sum_{i \in s} f(i) \right)^2}{\sum_{i \in s} g(i)} \leq \sum_{i \in s} \frac{f(i)^2}{g(i)}. \]

AbsoluteValue.sum_le theorem

 [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)

Full source

lemma AbsoluteValue.sum_le [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) :=
  Finset.le_sum_of_subadditive abv (map_zero _) abv.add_le _ _

Triangle Inequality for Absolute Value on Finite Sums

Informal description

Let $R$ and $S$ be semirings with $S$ partially ordered and an ordered ring structure. Given an absolute value function $\text{abv} : R \to S$, a finite set $s$ indexed by $\iota$, and a function $f : \iota \to R$, the absolute value of the sum of $f$ over $s$ is less than or equal to the sum of the absolute values of $f$ over $s$. That is, \[ \text{abv}\left(\sum_{i \in s} f(i)\right) \leq \sum_{i \in s} \text{abv}(f(i)). \]

IsAbsoluteValue.abv_sum theorem

 [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)

Full source

lemma IsAbsoluteValue.abv_sum [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) :=
  (IsAbsoluteValue.toAbsoluteValue abv).sum_le _ _

Triangle Inequality for Absolute Value on Finite Sums

Informal description

Let $R$ and $S$ be semirings with $S$ partially ordered and equipped with an ordered ring structure. Given an absolute value function $\text{abv} : R \to S$ and a finite set $s$ indexed by $\iota$, for any function $f : \iota \to R$, the absolute value of the sum of $f$ over $s$ is less than or equal to the sum of the absolute values of $f$ over $s$. That is, \[ \text{abv}\left(\sum_{i \in s} f(i)\right) \leq \sum_{i \in s} \text{abv}(f(i)). \]

AbsoluteValue.map_prod theorem

 [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)

Full source

nonrec lemma AbsoluteValue.map_prod [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) :=
  map_prod abv f s

Absolute Value Preserves Finite Products

Informal description

Let $R$ be a commutative semiring with a nontrivial structure, $S$ a commutative ring with a linear order and a strictly ordered ring structure, and $\text{abv} : R \to S$ an absolute value function. For any finite set $s$ indexed by $\iota$ and any function $f : \iota \to R$, the absolute value of the product of $f$ over $s$ is equal to the product of the absolute values of $f$ over $s$. That is, \[ \text{abv}\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} \text{abv}(f(i)). \]

IsAbsoluteValue.map_prod theorem

 [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)

Full source

lemma IsAbsoluteValue.map_prod [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) :=
  (IsAbsoluteValue.toAbsoluteValue abv).map_prod _ _

Absolute Value Preserves Finite Products

Informal description

Let $R$ be a commutative semiring with a nontrivial structure, $S$ a commutative ring with a linear order and a strictly ordered ring structure, and $\text{abv} : R \to S$ an absolute value function. For any finite set $s$ indexed by $\iota$ and any function $f : \iota \to R$, the absolute value of the product of $f$ over $s$ is equal to the product of the absolute values of $f$ over $s$. That is, \[ \text{abv}\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} \text{abv}(f(i)). \]

Mathlib.Meta.Positivity.evalFinsetProd definition

: PositivityExt

Full source

/-- 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.
-/
@[positivity Finset.prod _ _]
def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
  match e with
  | ~q(@Finset.prod $ι _ $instα $s $f) =>
    let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
    have body : Q($α) := Expr.betaRev f #[i]
    let rbody ← core zα pα body
    let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)

    -- Try to show that the product is positive
    let p_pos : Option Q(0 < $e) := ← do
      let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
      let .some _instαposmul ← trySynthInstanceQ q(PosMulStrictMono $α) | pure none
      let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
      assertInstancesCommute
      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
      return some q(prod_pos fun i _ ↦ $pr i)
    if let some p_pos := p_pos then return .positive p_pos

    -- Try to show that the product is nonnegative
    let p_nonneg : Option Q(0 ≤ $e) := ← do
      let .some pbody := rbody.toNonneg
        | return none -- Fail if the body is not provably nonnegative
      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
      let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
      assertInstancesCommute
      return some q(prod_nonneg fun i _ ↦ $pr i)
    if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg

    -- Fall back to showing that the product is nonzero
    let pbody ← rbody.toNonzero
    let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
    -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
    let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
    let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
    assertInstancesCommute
    return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)

Positivity extension for finite products

Informal description

The `positivity` extension proves that the product $\prod_{i \in s} f i$ is nonnegative if each $f i$ is nonnegative, and positive if each $f i$ is positive. It also handles the case where the product is nonzero if each $f i$ is nonzero.