Big operators on a finset in groups with zero involving order

This file contains the results concerning the interaction of finset big operators with groups with zero, where order is involved.

theorem Finset.prod_nonneg {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s : Finset ι} (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i

theorem Finset.prod_le_prod₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f g : ι → R} {s : Finset ι} (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

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.

theorem Monotone.finsetProd {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {s : Finset ι} {γ : Type u_3} [Preorder γ] {f : ι → γ → R} (hf : ∀ i ∈ s, Monotone (f i)) (hf₀ : ∀ i ∈ s, ∀ (x : γ), 0 ≤ f i x) : Monotone fun (x : γ) => ∏ i ∈ s, f i x

A finite product of nonnegative monotone functions is monotone. See also Monotone.finsetProd' for the case of an ordered commutative multiplicative monoid.

theorem MonotoneOn.finsetProd {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {s : Finset ι} {γ : Type u_3} [Preorder γ] {u : Set γ} {f : ι → γ → R} (hf : ∀ i ∈ s, MonotoneOn (f i) u) (hf₀ : ∀ i ∈ s, ∀ x ∈ u, 0 ≤ f i x) : MonotoneOn (fun (x : γ) => ∏ i ∈ s, f i x) u

A finite product of functions nonnegative and monotone on u is monotone on u. See also MonotoneOn.finsetProd' for the case of an ordered commutative multiplicative monoid.

theorem Antitone.finsetProd {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {s : Finset ι} {γ : Type u_3} [Preorder γ] {f : ι → γ → R} (hf : ∀ i ∈ s, Antitone (f i)) (hf₀ : ∀ i ∈ s, ∀ (x : γ), 0 ≤ f i x) : Antitone fun (x : γ) => ∏ i ∈ s, f i x

A finite product of nonnegative antitone functions is antitone. See also Antitone.finsetProd' for the case of an ordered commutative multiplicative monoid.

theorem AntitoneOn.finsetProd {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {s : Finset ι} {γ : Type u_3} [Preorder γ] {u : Set γ} {f : ι → γ → R} (hf : ∀ i ∈ s, AntitoneOn (f i) u) (hf₀ : ∀ i ∈ s, ∀ x ∈ u, 0 ≤ f i x) : AntitoneOn (fun (x : γ) => ∏ i ∈ s, f i x) u

A finite product of functions nonnegative and antitone on u is antitone on u. See also AntitoneOn.finsetProd' for the case of an ordered commutative multiplicative monoid.

theorem Finset.prod_le_one₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s : Finset ι} (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1

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.

theorem Finset.one_le_prod₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s : Finset ι} (hf : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i

A version of Finset.one_le_prod for PosMulMono in place of MulLeftMono.

theorem Finset.le_prod_max_one {ι : Type u_1} {s : Finset ι} {M : Type u_3} [CommMonoidWithZero M] [LinearOrder M] [ZeroLEOneClass M] [PosMulMono M] {i : ι} (hi : i ∈ s) (f : ι → M) : f i ≤ ∏ i ∈ s, max (f i) 1

theorem Finset.prod_mono_of_subset_of_one_le₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f g : ι → R} {s t : Finset ι} (h : s ⊆ t) (hf₀ : ∀ i ∈ s, 0 ≤ f i) (hfg : ∀ i ∈ s, f i ≤ g i) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, g i

theorem Finset.prod_mono_of_subset_of_le_one₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f g : ι → R} {s t : Finset ι} (h : s ⊆ t) (hg₀ : ∀ i ∈ t, 0 ≤ g i) (hgf : ∀ i ∈ s, g i ≤ f i) (hf : ∀ i ∈ t, i ∉ s → g i ≤ 1) : ∏ i ∈ t, g i ≤ ∏ i ∈ s, f i

theorem Finset.prod_le_prod_of_subset_of_one_le₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s t : Finset ι} (h : s ⊆ t) (hf₀ : ∀ i ∈ s, 0 ≤ f i) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

theorem Finset.prod_le_prod_of_subset_of_le_one₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s t : Finset ι} (h : s ⊆ t) (hf₀ : ∀ i ∈ t, 0 ≤ f i) (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) : ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i

theorem Finset.prod_mono_set_of_one_le₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} (hf : ∀ (x : ι), 1 ≤ f x) : Monotone fun (s : Finset ι) => ∏ x ∈ s, f x

theorem Finset.prod_anti_set_of_le_one₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} (hf0 : ∀ (x : ι), 0 ≤ f x) (hf : ∀ (x : ι), f x ≤ 1) : Antitone fun (s : Finset ι) => ∏ x ∈ s, f x

theorem Finset.prod_le_prod_of_injOn₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {α : Type u_3} [DecidableEq α] {g : α → R} {s : Finset ι} {t : Finset α} (e : ι → α) (he : Set.InjOn e ↑s) (ht : image e s ⊆ t) (h : ∀ i ∈ s, f i ≤ g (e i)) (hf0 : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ a ∈ t, a ∉ image e s → 1 ≤ g a) : ∏ i ∈ s, f i ≤ ∏ a ∈ t, g a

theorem Finset.prod_pos {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f : ι → R} {s : Finset ι} (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i

theorem Finset.prod_lt_prod₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι} (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

theorem Finset.prod_lt_prod_of_nonempty₀ {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι} (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