Results about big operators with values in an ordered algebraic structure.

Mostly monotonicity results for the ∏ and ∑ operations.

theorem Finset.le_sum_nonempty_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : M → N) (p : M → Prop) (h_mul : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) (hp_mul : (x y : M) → p x → p y → p (x + y)) (g : ι → M) (s : Finset ι) (hs_nonempty : Finset.Nonempty s) (hs : (i : ι) → i ∈ s → p (g i)) : f (Finset.sum s fun i => g i) ≤ Finset.sum s fun i => f (g i)

Let {x | p x} be an additive subsemigroup of an additive commutative monoid M. Let f : M → N be a map subadditive on {x | p x}, i.e., p x → p y → f (x + y) ≤ f x + f y. Let g i, i ∈ s, be a nonempty finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∑ i in s, g i) ≤ ∑ i in s, f (g i).

theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : M → N) (p : M → Prop) (h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) (hp_mul : (x y : M) → p x → p y → p (x * y)) (g : ι → M) (s : Finset ι) (hs_nonempty : Finset.Nonempty s) (hs : (i : ι) → i ∈ s → p (g i)) : f (Finset.prod s fun i => g i) ≤ Finset.prod s fun i => f (g i)

Let {x | p x} be a subsemigroup of a commutative monoid M. Let f : M → N be a map submultiplicative on {x | p x}, i.e., p x → p y → f (x * y) ≤ f x * f y. Let g i, i ∈ s, be a nonempty finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∏ x in s, g x) ≤ ∏ x in s, f (g x).

theorem Finset.le_sum_nonempty_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x + y) ≤ f x + f y) {s : Finset ι} (hs : Finset.Nonempty s) (g : ι → M) : f (Finset.sum s fun i => g i) ≤ Finset.sum s fun i => f (g i)

If f : M → N is a subadditive function, f (x + y) ≤ f x + f y and g i, i ∈ s, is a nonempty finite family of elements of M, then f (∑ i in s, g i) ≤ ∑ i in s, f (g i).

theorem Finset.le_prod_nonempty_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y) {s : Finset ι} (hs : Finset.Nonempty s) (g : ι → M) : f (Finset.prod s fun i => g i) ≤ Finset.prod s fun i => f (g i)

If f : M → N is a submultiplicative function, f (x * y) ≤ f x * f y and g i, i ∈ s, is a nonempty finite family of elements of M, then f (∏ i in s, g i) ≤ ∏ i in s, f (g i).

theorem Finset.le_sum_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : M → N) (p : M → Prop) (h_one : f 0 = 0) (h_mul : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) (hp_mul : (x y : M) → p x → p y → p (x + y)) (g : ι → M) {s : Finset ι} (hs : (i : ι) → i ∈ s → p (g i)) : f (Finset.sum s fun i => g i) ≤ Finset.sum s fun i => f (g i)

Let {x | p x} be a subsemigroup of a commutative additive monoid M. Let f : M → N be a map such that f 0 = 0 and f is subadditive on {x | p x}, i.e. p x → p y → f (x + y) ≤ f x + f y. Let g i, i ∈ s, be a finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∑ x in s, g x) ≤ ∑ x in s, f (g x).

theorem Finset.le_prod_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : M → N) (p : M → Prop) (h_one : f 1 = 1) (h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) (hp_mul : (x y : M) → p x → p y → p (x * y)) (g : ι → M) {s : Finset ι} (hs : (i : ι) → i ∈ s → p (g i)) : f (Finset.prod s fun i => g i) ≤ Finset.prod s fun i => f (g i)

Let {x | p x} be a subsemigroup of a commutative monoid M. Let f : M → N be a map such that f 1 = 1 and f is submultiplicative on {x | p x}, i.e., p x → p y → f (x * y) ≤ f x * f y. Let g i, i ∈ s, be a finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∏ i in s, g i) ≤ ∏ i in s, f (g i).

theorem Finset.le_sum_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : M → N) (h_one : f 0 = 0) (h_mul : ∀ (x y : M), f (x + y) ≤ f x + f y) (s : Finset ι) (g : ι → M) : f (Finset.sum s fun i => g i) ≤ Finset.sum s fun i => f (g i)

If f : M → N is a subadditive function, f (x + y) ≤ f x + f y, f 0 = 0, and g i, i ∈ s, is a finite family of elements of M, then f (∑ i in s, g i) ≤ ∑ i in s, f (g i).

theorem Finset.le_prod_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : M → N) (h_one : f 1 = 1) (h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) : f (Finset.prod s fun i => g i) ≤ Finset.prod s fun i => f (g i)

If f : M → N is a submultiplicative function, f (x * y) ≤ f x * f y, f 1 = 1, and g i, i ∈ s, is a finite family of elements of M, then f (∏ i in s, g i) ≤ ∏ i in s, f (g i).

theorem Finset.sum_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : (Finset.sum s fun i => f i) ≤ Finset.sum s fun i => g i

In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then ∑ i in s, f i ≤ ∑ i in s, g i.

theorem Finset.prod_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : (Finset.prod s fun i => f i) ≤ Finset.prod s fun i => g i

In an ordered commutative monoid, if each factor f i of one finite product is less than or equal to the corresponding factor g i of another finite product, then ∏ i in s, f i ≤ ∏ i in s, g i.

theorem GCongr.sum_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : Finset.sum s f ≤ Finset.sum s g

In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then s.sum f ≤ s.sum g.

This is a variant (beta-reduced) version of the standard lemma Finset.sum_le_sum, convenient for the gcongr tactic.

theorem GCongr.prod_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : Finset.prod s f ≤ Finset.prod s g

In an ordered commutative monoid, if each factor f i of one finite product is less than or equal to the corresponding factor g i of another finite product, then s.prod f ≤ s.prod g.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_le_prod', convenient for the gcongr tactic.

theorem Finset.sum_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → 0 ≤ f i) : 0 ≤ Finset.sum s fun i => f i

theorem Finset.one_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → 1 ≤ f i) : 1 ≤ Finset.prod s fun i => f i

theorem Finset.sum_nonneg' {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), 0 ≤ f i) : 0 ≤ Finset.sum s fun i => f i

theorem Finset.one_le_prod'' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), 1 ≤ f i) : 1 ≤ Finset.prod s fun i => f i

theorem Finset.sum_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ 0) : (Finset.sum s fun i => f i) ≤ 0

theorem Finset.prod_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ 1) : (Finset.prod s fun i => f i) ≤ 1

theorem Finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) (hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 0 ≤ f i) : (Finset.sum s fun i => f i) ≤ Finset.sum t fun i => f i

theorem Finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) (hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) : (Finset.prod s fun i => f i) ≤ Finset.prod t fun i => f i

theorem Finset.sum_mono_set_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} (hf : ∀ (x : ι), 0 ≤ f x) : Monotone fun s => Finset.sum s fun x => f x

theorem Finset.prod_mono_set_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} (hf : ∀ (x : ι), 1 ≤ f x) : Monotone fun s => Finset.prod s fun x => f x

theorem Finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 0 ≤ f x) : (Finset.sum s fun x => f x) ≤ Finset.sum Finset.univ fun x => f x

theorem Finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 1 ≤ f x) : (Finset.prod s fun x => f x) ≤ Finset.prod Finset.univ fun x => f x

theorem Finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ (i : ι), i ∈ s → 0 ≤ f i) → ((Finset.sum s fun i => f i) = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)

theorem Finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ (i : ι), i ∈ s → 1 ≤ f i) → ((Finset.prod s fun i => f i) = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

theorem Finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ (i : ι), i ∈ s → f i ≤ 1) → ((Finset.prod s fun i => f i) = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

theorem Finset.single_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (hf : ∀ (i : ι), i ∈ s → 0 ≤ f i) {a : ι} (h : a ∈ s) : f a ≤ Finset.sum s fun x => f x

theorem Finset.single_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (hf : ∀ (i : ι), i ∈ s → 1 ≤ f i) {a : ι} (h : a ∈ s) : f a ≤ Finset.prod s fun x => f x

theorem Finset.sum_le_card_nsmul {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x ∈ s → f x ≤ n) : Finset.sum s f ≤ Finset.card s • n

theorem Finset.prod_le_pow_card {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x ∈ s → f x ≤ n) : Finset.prod s f ≤ n ^ Finset.card s

theorem Finset.card_nsmul_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x ∈ s → n ≤ f x) : Finset.card s • n ≤ Finset.sum s f

theorem Finset.pow_card_le_prod {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x ∈ s → n ≤ f x) : n ^ Finset.card s ≤ Finset.prod s f

theorem Finset.card_biUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ) (h : ∀ (a : ι), a ∈ s → Finset.card (f a) ≤ n) : Finset.card (Finset.biUnion s f) ≤ Finset.card s * n

theorem Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), ¬y ∈ t → 0 ≤ Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x) : (Finset.sum t fun y => Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x) ≤ Finset.sum s fun x => f x

theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), ¬y ∈ t → 1 ≤ Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x) : (Finset.prod t fun y => Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x) ≤ Finset.prod s fun x => f x

theorem Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), ¬y ∈ t → (Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x) ≤ 0) : (Finset.sum s fun x => f x) ≤ Finset.sum t fun y => Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x

theorem Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), ¬y ∈ t → (Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x) ≤ 1) : (Finset.prod s fun x => f x) ≤ Finset.prod t fun y => Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x

theorem Finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] (f : ι → G) (s : Finset ι) : |Finset.sum s fun i => f i| ≤ Finset.sum s fun i => |f i|

theorem Finset.abs_sum_of_nonneg {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] {f : ι → G} {s : Finset ι} (hf : ∀ (i : ι), i ∈ s → 0 ≤ f i) : |Finset.sum s fun i => f i| = Finset.sum s fun i => f i

theorem Finset.abs_sum_of_nonneg' {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] {f : ι → G} {s : Finset ι} (hf : ∀ (i : ι), 0 ≤ f i) : |Finset.sum s fun i => f i| = Finset.sum s fun i => f i

theorem Finset.abs_prod {ι : Type u_1} {R : Type u_9} [LinearOrderedCommRing R] {f : ι → R} {s : Finset ι} : |Finset.prod s fun x => f x| = Finset.prod s fun x => |f x|

theorem Finset.card_le_mul_card_image_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ (a : α), a ∈ s → f a ∈ t) (n : ℕ) (hn : ∀ (a : β), a ∈ t → Finset.card (Finset.filter (fun x => f x = a) s) ≤ n) : Finset.card s ≤ n * Finset.card t

theorem Finset.card_le_mul_card_image {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ (a : β), a ∈ Finset.image f s → Finset.card (Finset.filter (fun x => f x = a) s) ≤ n) : Finset.card s ≤ n * Finset.card (Finset.image f s)

theorem Finset.mul_card_image_le_card_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ (a : α), a ∈ s → f a ∈ t) (n : ℕ) (hn : ∀ (a : β), a ∈ t → n ≤ Finset.card (Finset.filter (fun x => f x = a) s)) : n * Finset.card t ≤ Finset.card s

theorem Finset.mul_card_image_le_card {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ (a : β), a ∈ Finset.image f s → n ≤ Finset.card (Finset.filter (fun x => f x = a) s)) : n * Finset.card (Finset.image f s) ≤ Finset.card s

theorem Finset.sum_card_inter_le {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ (a : α), a ∈ s → Finset.card (Finset.filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n) : (Finset.sum B fun t => Finset.card (s ∩ t)) ≤ Finset.card s * n

If every element belongs to at most n Finsets, then the sum of their sizes is at most n times how many they are.

theorem Finset.sum_card_le {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), Finset.card (Finset.filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n) : (Finset.sum B fun s => Finset.card s) ≤ Fintype.card α * n

If every element belongs to at most n Finsets, then the sum of their sizes is at most n times how many they are.

theorem Finset.le_sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ (a : α), a ∈ s → n ≤ Finset.card (Finset.filter ((fun x x_1 => x ∈ x_1) a) B)) : Finset.card s * n ≤ Finset.sum B fun t => Finset.card (s ∩ t)

If every element belongs to at least n Finsets, then the sum of their sizes is at least n times how many they are.

theorem Finset.le_sum_card {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), n ≤ Finset.card (Finset.filter ((fun x x_1 => x ∈ x_1) a) B)) : Fintype.card α * n ≤ Finset.sum B fun s => Finset.card s

If every element belongs to at least n Finsets, then the sum of their sizes is at least n times how many they are.

theorem Finset.sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ (a : α), a ∈ s → Finset.card (Finset.filter ((fun x x_1 => x ∈ x_1) a) B) = n) : (Finset.sum B fun t => Finset.card (s ∩ t)) = Finset.card s * n

If every element belongs to exactly n Finsets, then the sum of their sizes is n times how many they are.

theorem Finset.sum_card {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), Finset.card (Finset.filter ((fun x x_1 => x ∈ x_1) a) B) = n) : (Finset.sum B fun s => Finset.card s) = Fintype.card α * n

If every element belongs to exactly n Finsets, then the sum of their sizes is n times how many they are.

theorem Finset.card_le_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : Set.PairwiseDisjoint (↑s) f) (hf : ∀ (i : ι), i ∈ s → Finset.Nonempty (f i)) : Finset.card s ≤ Finset.card (Finset.biUnion s f)

theorem Finset.card_le_card_biUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : Set.PairwiseDisjoint (↑s) f) : Finset.card s ≤ Finset.card (Finset.biUnion s f) + Finset.card (Finset.filter (fun i => f i = ∅) s)

theorem Finset.card_le_card_biUnion_add_one {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hf : Function.Injective f) (hs : Set.PairwiseDisjoint (↑s) f) : Finset.card s ≤ Finset.card (Finset.biUnion s f) + 1

@[simp]

theorem Finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddMonoid M] {f : ι → M} {s : Finset ι} : (Finset.sum s fun x => f x) = 0 ↔ ∀ (x : ι), x ∈ s → f x = 0

@[simp]

theorem Finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] {f : ι → M} {s : Finset ι} : (Finset.prod s fun x => f x) = 1 ↔ ∀ (x : ι), x ∈ s → f x = 1

theorem Finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) : (Finset.sum s fun x => f x) ≤ Finset.sum t fun x => f x

theorem Finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) : (Finset.prod s fun x => f x) ≤ Finset.prod t fun x => f x

theorem Finset.sum_mono_set {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddMonoid M] (f : ι → M) : Monotone fun s => Finset.sum s fun x => f x

theorem Finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] (f : ι → M) : Monotone fun s => Finset.prod s fun x => f x

theorem Finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : ∀ (x : ι), x ∈ s → f x ≠ 0 → x ∈ t) : (Finset.sum s fun x => f x) ≤ Finset.sum t fun x => f x

theorem Finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t) : (Finset.prod s fun x => f x) ≤ Finset.prod t fun x => f x

theorem Finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (Hle : ∀ (i : ι), i ∈ s → f i ≤ g i) (Hlt : ∃ i, i ∈ s ∧ f i < g i) : (Finset.sum s fun i => f i) < Finset.sum s fun i => g i

theorem Finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (Hle : ∀ (i : ι), i ∈ s → f i ≤ g i) (Hlt : ∃ i, i ∈ s ∧ f i < g i) : (Finset.prod s fun i => f i) < Finset.prod s fun i => g i

theorem Finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : Finset.Nonempty s) (Hlt : ∀ (i : ι), i ∈ s → f i < g i) : (Finset.sum s fun i => f i) < Finset.sum s fun i => g i

theorem Finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : Finset.Nonempty s) (Hlt : ∀ (i : ι), i ∈ s → f i < g i) : (Finset.prod s fun i => f i) < Finset.prod s fun i => g i

theorem GCongr.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : Finset.Nonempty s) (Hlt : ∀ (i : ι), i ∈ s → f i < g i) : Finset.sum s f < Finset.sum s g

In an ordered additive commutative monoid, if each summand f i of one nontrivial finite sum is strictly less than the corresponding summand g i of another nontrivial finite sum, then s.sum f < s.sum g.

This is a variant (beta-reduced) version of the standard lemma Finset.sum_lt_sum_of_nonempty, convenient for the gcongr tactic.

theorem GCongr.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : Finset.Nonempty s) (Hlt : ∀ (i : ι), i ∈ s → f i < g i) : Finset.prod s f < Finset.prod s g

In an ordered commutative monoid, if each factor f i of one nontrivial finite product is strictly less than the corresponding factor g i of another nontrivial finite product, then s.prod f < s.prod g.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_lt_prod_of_nonempty', convenient for the gcongr tactic.

theorem Finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : ¬i ∈ s) (hlt : 0 < f i) (hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 0 ≤ f j) : (Finset.sum s fun j => f j) < Finset.sum t fun j => f j

theorem Finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : ¬i ∈ s) (hlt : 1 < f i) (hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j) : (Finset.prod s fun j => f j) < Finset.prod t fun j => f j

theorem Finset.single_lt_sum {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} {i : ι} {j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 0 < f j) (hle : ∀ (k : ι), k ∈ s → k ≠ i → 0 ≤ f k) : f i < Finset.sum s fun k => f k

theorem Finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} {i : ι} {j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j) (hle : ∀ (k : ι), k ∈ s → k ≠ i → 1 ≤ f k) : f i < Finset.prod s fun k => f k

theorem Finset.sum_pos {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → 0 < f i) (hs : Finset.Nonempty s) : 0 < Finset.sum s fun i => f i

theorem Finset.one_lt_prod {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → 1 < f i) (hs : Finset.Nonempty s) : 1 < Finset.prod s fun i => f i

theorem Finset.sum_neg {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i < 0) (hs : Finset.Nonempty s) : (Finset.sum s fun i => f i) < 0

theorem Finset.prod_lt_one {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i < 1) (hs : Finset.Nonempty s) : (Finset.prod s fun i => f i) < 1

theorem Finset.sum_pos' {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → 0 ≤ f i) (hs : ∃ i, i ∈ s ∧ 0 < f i) : 0 < Finset.sum s fun i => f i

theorem Finset.one_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → 1 ≤ f i) (hs : ∃ i, i ∈ s ∧ 1 < f i) : 1 < Finset.prod s fun i => f i

theorem Finset.sum_neg' {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ 0) (hs : ∃ i, i ∈ s ∧ f i < 0) : (Finset.sum s fun i => f i) < 0

theorem Finset.prod_lt_one' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ (i : ι), i ∈ s → f i ≤ 1) (hs : ∃ i, i ∈ s ∧ f i < 1) : (Finset.prod s fun i => f i) < 1

theorem Finset.sum_eq_sum_iff_of_le {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {s : Finset ι} {f : ι → M} {g : ι → M} (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : ((Finset.sum s fun i => f i) = Finset.sum s fun i => g i) ↔ ∀ (i : ι), i ∈ s → f i = g i

theorem Finset.prod_eq_prod_iff_of_le {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {s : Finset ι} {f : ι → M} {g : ι → M} (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : ((Finset.prod s fun i => f i) = Finset.prod s fun i => g i) ↔ ∀ (i : ι), i ∈ s → f i = g i

theorem Finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (Hlt : (Finset.sum s fun i => f i) < Finset.sum s fun i => g i) : ∃ i, i ∈ s ∧ f i < g i

theorem Finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (Hlt : (Finset.prod s fun i => f i) < Finset.prod s fun i => g i) : ∃ i, i ∈ s ∧ f i < g i

theorem Finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : Finset.Nonempty s) (Hle : (Finset.sum s fun i => f i) ≤ Finset.sum s fun i => g i) : ∃ i, i ∈ s ∧ f i ≤ g i

theorem Finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : Finset.Nonempty s) (Hle : (Finset.prod s fun i => f i) ≤ Finset.prod s fun i => g i) : ∃ i, i ∈ s ∧ f i ≤ g i

theorem Finset.exists_pos_of_sum_zero_of_exists_nonzero {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {s : Finset ι} (f : ι → M) (h₁ : (Finset.sum s fun i => f i) = 0) (h₂ : ∃ i, i ∈ s ∧ f i ≠ 0) : ∃ i, i ∈ s ∧ 0 < f i

theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {s : Finset ι} (f : ι → M) (h₁ : (Finset.prod s fun i => f i) = 1) (h₂ : ∃ i, i ∈ s ∧ f i ≠ 1) : ∃ i, i ∈ s ∧ 1 < f i

theorem Finset.prod_nonneg {ι : Type u_1} {R : Type u_8} [OrderedCommSemiring R] {f : ι → R} {s : Finset ι} (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) : 0 ≤ Finset.prod s fun i => f i

theorem Finset.prod_le_prod {ι : Type u_1} {R : Type u_8} [OrderedCommSemiring R] {f : ι → R} {g : ι → R} {s : Finset ι} (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h1 : ∀ (i : ι), i ∈ s → f i ≤ g i) : (Finset.prod s fun i => f i) ≤ Finset.prod s fun i => 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 GCongr.prod_le_prod {ι : Type u_1} {R : Type u_8} [OrderedCommSemiring R] {f : ι → R} {g : ι → R} {s : Finset ι} (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h1 : ∀ (i : ι), i ∈ s → f i ≤ g i) : Finset.prod s f ≤ Finset.prod s g

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.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_le_prod, convenient for the gcongr tactic.

theorem Finset.prod_le_one {ι : Type u_1} {R : Type u_8} [OrderedCommSemiring R] {f : ι → R} {s : Finset ι} (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h1 : ∀ (i : ι), i ∈ s → f i ≤ 1) : (Finset.prod s fun i => 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.prod_add_prod_le {ι : Type u_1} {R : Type u_8} [OrderedCommSemiring R] {s : Finset ι} {i : ι} {f : ι → R} {g : ι → R} {h : ι → R} (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j) (hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j) (hg : ∀ (i : ι), i ∈ s → 0 ≤ g i) (hh : ∀ (i : ι), i ∈ s → 0 ≤ h i) : ((Finset.prod s fun i => g i) + Finset.prod s fun i => h i) ≤ Finset.prod s fun i => f i

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.

theorem Finset.prod_pos {ι : Type u_1} {R : Type u_8} [StrictOrderedCommSemiring R] [Nontrivial R] {f : ι → R} {s : Finset ι} (h0 : ∀ (i : ι), i ∈ s → 0 < f i) : 0 < Finset.prod s fun i => f i

@[simp]

theorem CanonicallyOrderedCommSemiring.prod_pos {ι : Type u_1} {R : Type u_8} [CanonicallyOrderedCommSemiring R] {f : ι → R} {s : Finset ι} [Nontrivial R] : (0 < Finset.prod s fun i => f i) ↔ ∀ (i : ι), i ∈ s → 0 < f i

Note that the name is to match CanonicallyOrderedCommSemiring.mul_pos.

theorem Finset.prod_add_prod_le' {ι : Type u_1} {R : Type u_8} [CanonicallyOrderedCommSemiring R] {f : ι → R} {g : ι → R} {h : ι → R} {s : Finset ι} {i : ι} (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j) (hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j) : ((Finset.prod s fun i => g i) + Finset.prod s fun i => h i) ≤ Finset.prod s fun i => f i

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 CanonicallyOrderedCommSemiring.

theorem Fintype.sum_mono {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] : Monotone fun f => Finset.sum Finset.univ fun i => f i

theorem Fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] : Monotone fun f => Finset.prod Finset.univ fun i => f i

theorem Fintype.sum_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : 0 ≤ Finset.sum Finset.univ fun i => f i

theorem Fintype.one_le_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : 1 ≤ Finset.prod Finset.univ fun i => f i

theorem Fintype.sum_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : (Finset.sum Finset.univ fun i => f i) ≤ 0

theorem Fintype.prod_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : f ≤ 1) : (Finset.prod Finset.univ fun i => f i) ≤ 1

theorem Fintype.sum_strictMono {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] : StrictMono fun f => Finset.sum Finset.univ fun x => f x

abbrev Fintype.sum_strictMono.match_1 {ι : Type u_1} {M : Type u_2} [OrderedCancelAddCommMonoid M] : (x x_1 : ι → M) → (motive : (x ≤ x_1 ∧ ∃ i, x i < x_1 i) → Prop) → ∀ (x_2 : x ≤ x_1 ∧ ∃ i, x i < x_1 i), (∀ (hle : x ≤ x_1) (i : ι) (hlt : x i < x_1 i), motive (_ : x ≤ x_1 ∧ ∃ i, x i < x_1 i)) → motive x_2

Equations

• Fintype.sum_strictMono.match_1 x x motive x h_1 = And.casesOn x fun left right => Exists.casesOn right fun w h => h_1 left w h

theorem Fintype.prod_strictMono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] : StrictMono fun f => Finset.prod Finset.univ fun x => f x

theorem Fintype.sum_pos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : 0 < f) : 0 < Finset.sum Finset.univ fun i => f i

theorem Fintype.one_lt_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : 1 < f) : 1 < Finset.prod Finset.univ fun i => f i

theorem Fintype.sum_neg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : f < 0) : (Finset.sum Finset.univ fun i => f i) < 0

theorem Fintype.prod_lt_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : f < 1) : (Finset.prod Finset.univ fun i => f i) < 1

theorem Fintype.sum_pos_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : (0 < Finset.sum Finset.univ fun i => f i) ↔ 0 < f

theorem Fintype.one_lt_prod_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : (1 < Finset.prod Finset.univ fun i => f i) ↔ 1 < f

theorem Fintype.sum_neg_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : (Finset.sum Finset.univ fun i => f i) < 0 ↔ f < 0

theorem Fintype.prod_lt_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : f ≤ 1) : (Finset.prod Finset.univ fun i => f i) < 1 ↔ f < 1

theorem Fintype.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : (Finset.sum Finset.univ fun i => f i) = 0 ↔ f = 0

theorem Fintype.prod_eq_one_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : (Finset.prod Finset.univ fun i => f i) = 1 ↔ f = 1

theorem Fintype.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : (Finset.sum Finset.univ fun i => f i) = 0 ↔ f = 0

theorem Fintype.prod_eq_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : f ≤ 1) : (Finset.prod Finset.univ fun i => f i) = 1 ↔ f = 1

theorem WithTop.prod_lt_top {ι : Type u_1} {R : Type u_8} [CommMonoidWithZero R] [NoZeroDivisors R] [Nontrivial R] [DecidableEq R] [LT R] {s : Finset ι} {f : ι → WithTop R} (h : ∀ (i : ι), i ∈ s → f i ≠ ⊤) : (Finset.prod s fun i => f i) < ⊤

A product of finite numbers is still finite

theorem WithTop.sum_eq_top_iff {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → WithTop M} : (Finset.sum s fun i => f i) = ⊤ ↔ ∃ i, i ∈ s ∧ f i = ⊤

A sum of numbers is infinite iff one of them is infinite

theorem WithTop.sum_lt_top_iff {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LT M] {s : Finset ι} {f : ι → WithTop M} : (Finset.sum s fun i => f i) < ⊤ ↔ ∀ (i : ι), i ∈ s → f i < ⊤

A sum of finite numbers is still finite

theorem WithTop.sum_lt_top {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LT M] {s : Finset ι} {f : ι → WithTop M} (h : ∀ (i : ι), i ∈ s → f i ≠ ⊤) : (Finset.sum s fun i => f i) < ⊤

A sum of finite numbers is still finite

theorem AbsoluteValue.sum_le {ι : Type u_1} {R : Type u_8} {S : Type u_9} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) (s : Finset ι) (f : ι → R) : ↑abv (Finset.sum s fun i => f i) ≤ Finset.sum s fun i => ↑abv (f i)

theorem IsAbsoluteValue.abv_sum {ι : Type u_1} {R : Type u_8} {S : Type u_9} [Semiring R] [OrderedSemiring S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) : abv (Finset.sum s fun i => f i) ≤ Finset.sum s fun i => abv (f i)

theorem AbsoluteValue.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S] (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι) : ↑abv (Finset.prod s fun i => f i) = Finset.prod s fun i => ↑abv (f i)

theorem IsAbsoluteValue.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι) : abv (Finset.prod s fun i => f i) = Finset.prod s fun i => abv (f i)