Products of antitone sequences over finite sets of indices

For a nonnegative antitone sequence f : ℕ → R in an ordered commutative monoid with zero, the product of f over a finite set s of indices is largest when s is an initial segment: it is at most the product over range #s (Finset.prod_le_prod_range_card). More generally, the product over s is at most the product over any set t of the same size having, below every threshold, at least as many indices as s (Finset.prod_le_prod_of_card_filter_lt_le). If s has n + 1 elements and is not the initial segment range (n + 1), then it contains an index at least n + 1, and its product is at most (∏ i ∈ range n, f i) * f (n + 1) (Finset.prod_le_prod_range_mul_of_not_subset). For a strictly decreasing positive sequence the right-hand side is strictly smaller than the product over range (n + 1), which gives an explicit gap between the initial segment and every other set of the same size. This is how a dominant term is singled out among the products of n entries of a decreasing sequence of norms.

theorem Finset.prod_le_prod_of_card_filter_lt_le {R : Type u_1} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ℕ → R} (hf₀ : ∀ (i : ℕ), 0 ≤ f i) (hf : Antitone f) {s t : Finset ℕ} (hst : s.card = t.card) (h : ∀ (k : ℕ), {i ∈ s | i < k}.card ≤ {i ∈ t | i < k}.card) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Products along a count domination. For a nonnegative antitone sequence f, let s and t be finite sets of indices of the same size such that, below every threshold k, s has at most as many indices as t. Then the product of f over s is at most its product over t.

theorem Finset.prod_le_prod_range_card {R : Type u_1} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ℕ → R} (hf₀ : ∀ (i : ℕ), 0 ≤ f i) (hf : Antitone f) (s : Finset ℕ) : ∏ i ∈ s, f i ≤ ∏ i ∈ range s.card, f i

For a nonnegative antitone sequence f, the product of f over a finite set s of indices is at most its product over the initial segment range #s of the same size.

theorem Finset.prod_le_prod_range_mul_of_not_subset {R : Type u_1} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ℕ → R} (hf₀ : ∀ (i : ℕ), 0 ≤ f i) (hf : Antitone f) {s : Finset ℕ} {n : ℕ} (hs : s.card = n + 1) (hsub : ¬s ⊆ range (n + 1)) : ∏ i ∈ s, f i ≤ (∏ i ∈ range n, f i) * f (n + 1)

For a nonnegative antitone sequence f, a set s of n + 1 indices that is not contained in the initial segment range (n + 1) has product at most (∏ i ∈ range n, f i) * f (n + 1).