Sums with weights in the unit interval

A sum ∑ i ∈ s, f i * c i with weights 0 ≤ f i ≤ 1 lies between the sum of the negative terms of c and the sum of its positive terms. Both are sums of c over subsets of s, so any bound on the absolute values of all subset sums of c also bounds every such weighted sum. Applying this once in each variable gives the corresponding statement for a matrix w tested against two weight vectors.

In regularity arguments this upgrades a discrepancy bound on rectangles s' × t' to one for tests f i * g j with values in [0, 1], as needed for counting lemmas. Summing such a bound over a further index then uses the crude estimate |∑ i ∈ s, f i| ≤ #s • B for terms bounded by B in absolute value.

Main results

• Finset.abs_sum_mul_le_of_forall_subset: weighted sums are controlled by subset sums.
• Finset.abs_sum_sum_mul_mul_le_of_forall_subset: the two-variable version.
• Finset.abs_sum_le_card_nsmul: a sum of #s terms bounded by B in absolute value is bounded by #s • B.

theorem Finset.abs_sum_mul_le_of_forall_subset {ι : Type u_1} {R : Type u_3} [Ring R] [LinearOrder R] [IsOrderedRing R] {s : Finset ι} {f c : ι → R} {M : R} (hf₀ : ∀ i ∈ s, 0 ≤ f i) (hf₁ : ∀ i ∈ s, f i ≤ 1) (h : ∀ t ⊆ s, |∑ i ∈ t, c i| ≤ M) : |∑ i ∈ s, f i * c i| ≤ M

If every subset sum of c over s has absolute value at most M, then so has every sum ∑ i ∈ s, f i * c i with weights 0 ≤ f i ≤ 1.

theorem Finset.abs_sum_sum_mul_mul_le_of_forall_subset {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Ring R] [LinearOrder R] [IsOrderedRing R] {s : Finset ι} {t : Finset κ} {f : ι → R} {g : κ → R} {w : ι → κ → R} {M : R} (hf₀ : ∀ i ∈ s, 0 ≤ f i) (hf₁ : ∀ i ∈ s, f i ≤ 1) (hg₀ : ∀ j ∈ t, 0 ≤ g j) (hg₁ : ∀ j ∈ t, g j ≤ 1) (h : ∀ s' ⊆ s, ∀ t' ⊆ t, |∑ i ∈ s', ∑ j ∈ t', w i j| ≤ M) : |∑ i ∈ s, ∑ j ∈ t, f i * g j * w i j| ≤ M

If every rectangle sum ∑ i ∈ s', ∑ j ∈ t', w i j with s' ⊆ s and t' ⊆ t has absolute value at most M, then so has every sum ∑ i ∈ s, ∑ j ∈ t, f i * g j * w i j with weights in [0, 1].

theorem Finset.abs_sum_le_card_nsmul {ι : Type u_1} {R : Type u_3} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {s : Finset ι} {f : ι → R} {B : R} (h : ∀ i ∈ s, |f i| ≤ B) : |∑ i ∈ s, f i| ≤ s.card • B

A sum of terms with absolute value at most B has absolute value at most #s • B.