Magnitudes of finite sums and products

Main results

• Finset.abs_sum_mul_le: bounded signed linear combinations.
• Finset.abs_prod_le_one: products of coefficients bounded by one.

References

Adapted selectively from Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

theorem Finset.abs_sum_le_card_mul {ι : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] (s : Finset ι) {f : ι → R} {A : R} (h : ∀ i ∈ s, |f i| ≤ A) : |∑ i ∈ s, f i| ≤ ↑s.card * A

If |f i| ≤ A for all i ∈ s, then |∑ i ∈ s, f i| ≤ s.card * A.

theorem Finset.abs_sum_mul_le {ι : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] (s : Finset ι) {c a : ι → R} {A : R} (hc : ∀ i ∈ s, |c i| ≤ 1) (ha : ∀ i ∈ s, |a i| ≤ A) : |∑ i ∈ s, c i * a i| ≤ ↑s.card * A

If |c i| ≤ 1 and |a i| ≤ A for all i ∈ s, then |∑ i ∈ s, c i * a i| ≤ s.card * A.

theorem Finset.abs_prod_le_one {ι : Type u_1} {R : Type u_2} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι) {f : ι → R} (h : ∀ i ∈ s, |f i| ≤ 1) : |∏ i ∈ s, f i| ≤ 1

If |f i| ≤ 1 for all i ∈ s, then |∏ i ∈ s, f i| ≤ 1.