mathlib documentation

algebra.big_operators.order

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

Mostly monotonicity results for the operation.

theorem finset.le_sum_of_subadditive {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid α] [ordered_add_comm_monoid β] (f : α → β) (h_zero : f 0 = 0) (h_add : ∀ (x y : α), f (x + y) f x + f y) (s : finset γ) (g : γ → α) :
f (∑ (x : γ) in s, g x) ∑ (x : γ) in s, f (g x)

theorem finset.abs_sum_le_sum_abs {α : Type u} {β : Type v} [linear_ordered_field α] {f : β → α} {s : finset β} :
abs (∑ (x : β) in s, f x) ∑ (x : β) in s, abs (f x)

theorem finset.sum_le_sum {α : Type u} {β : Type v} {s : finset α} {f g : α → β} [ordered_add_comm_monoid β] :
(∀ (x : α), x sf x g x)∑ (x : α) in s, f x ∑ (x : α) in s, g x

theorem finset.card_le_mul_card_image_of_maps_to {α : Type u} {γ : Type w} [decidable_eq γ] {f : α → γ} {s : finset α} {t : finset γ} (Hf : ∀ (a : α), a sf a t) (n : ) :
(∀ (a : γ), a t(finset.filter (λ (x : α), f x = a) s).card n)s.card n * t.card

theorem finset.card_le_mul_card_image {α : Type u} {γ : Type w} [decidable_eq γ] {f : α → γ} (s : finset α) (n : ) :
(∀ (a : γ), a finset.image f s(finset.filter (λ (x : α), f x = a) s).card n)s.card n * (finset.image f s).card

theorem finset.mul_card_image_le_card_of_maps_to {α : Type u} {γ : Type w} [decidable_eq γ] {f : α → γ} {s : finset α} {t : finset γ} (Hf : ∀ (a : α), a sf a t) (n : ) :
(∀ (a : γ), a tn (finset.filter (λ (x : α), f x = a) s).card)n * t.card s.card

theorem finset.mul_card_image_le_card {α : Type u} {γ : Type w} [decidable_eq γ] {f : α → γ} (s : finset α) (n : ) :
(∀ (a : γ), a finset.image f sn (finset.filter (λ (x : α), f x = a) s).card)n * (finset.image f s).card s.card

theorem finset.sum_nonneg {α : Type u} {β : Type v} {s : finset α} {f : α → β} [ordered_add_comm_monoid β] :
(∀ (x : α), x s0 f x)0 ∑ (x : α) in s, f x

theorem finset.sum_nonpos {α : Type u} {β : Type v} {s : finset α} {f : α → β} [ordered_add_comm_monoid β] :
(∀ (x : α), x sf x 0)∑ (x : α) in s, f x 0

theorem finset.sum_le_sum_of_subset_of_nonneg {α : Type u} {β : Type v} {s₁ s₂ : finset α} {f : α → β} [ordered_add_comm_monoid β] :
s₁ s₂(∀ (x : α), x s₂x s₁0 f x)∑ (x : α) in s₁, f x ∑ (x : α) in s₂, f x

theorem finset.sum_mono_set_of_nonneg {α : Type u} {β : Type v} {f : α → β} [ordered_add_comm_monoid β] :
(∀ (x : α), 0 f x)monotone (λ (s : finset α), ∑ (x : α) in s, f x)

theorem finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {α : Type u} {β : Type v} {γ : Type w} [ordered_add_comm_monoid β] [decidable_eq γ] {s : finset α} {t : finset γ} {g : α → γ} {f : α → β} :
(∀ (y : γ), y t0 ∑ (x : α) in finset.filter (λ (x : α), g x = y) s, f x)∑ (y : γ) in t, ∑ (x : α) in finset.filter (λ (x : α), g x = y) s, f x ∑ (x : α) in s, f x

theorem finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {α : Type u} {β : Type v} {γ : Type w} [ordered_add_comm_monoid β] [decidable_eq γ] {s : finset α} {t : finset γ} {g : α → γ} {f : α → β} :
(∀ (y : γ), y t∑ (x : α) in finset.filter (λ (x : α), g x = y) s, f x 0)∑ (x : α) in s, f x ∑ (y : γ) in t, ∑ (x : α) in finset.filter (λ (x : α), g x = y) s, f x

theorem finset.sum_eq_zero_iff_of_nonneg {α : Type u} {β : Type v} {s : finset α} {f : α → β} [ordered_add_comm_monoid β] :
(∀ (x : α), x s0 f x)(∑ (x : α) in s, f x = 0 ∀ (x : α), x sf x = 0)

theorem finset.sum_eq_zero_iff_of_nonpos {α : Type u} {β : Type v} {s : finset α} {f : α → β} [ordered_add_comm_monoid β] :
(∀ (x : α), x sf x 0)(∑ (x : α) in s, f x = 0 ∀ (x : α), x sf x = 0)

theorem finset.single_le_sum {α : Type u} {β : Type v} {s : finset α} {f : α → β} [ordered_add_comm_monoid β] (hf : ∀ (x : α), x s0 f x) {a : α} :
a sf a ∑ (x : α) in s, f x

@[simp]
theorem finset.sum_eq_zero_iff {α : Type u} {β : Type v} {s : finset α} {f : α → β} [canonically_ordered_add_monoid β] :
∑ (x : α) in s, f x = 0 ∀ (x : α), x sf x = 0

theorem finset.sum_le_sum_of_subset {α : Type u} {β : Type v} {s₁ s₂ : finset α} {f : α → β} [canonically_ordered_add_monoid β] :
s₁ s₂∑ (x : α) in s₁, f x ∑ (x : α) in s₂, f x

theorem finset.sum_mono_set {α : Type u} {β : Type v} [canonically_ordered_add_monoid β] (f : α → β) :
monotone (λ (s : finset α), ∑ (x : α) in s, f x)

theorem finset.sum_le_sum_of_ne_zero {α : Type u} {β : Type v} {s₁ s₂ : finset α} {f : α → β} [canonically_ordered_add_monoid β] :
(∀ (x : α), x s₁f x 0x s₂)∑ (x : α) in s₁, f x ∑ (x : α) in s₂, f x

theorem finset.sum_lt_sum {α : Type u} {β : Type v} {s : finset α} {f g : α → β} [ordered_cancel_add_comm_monoid β] :
(∀ (i : α), i sf i g i)(∃ (i : α) (H : i s), f i < g i)∑ (x : α) in s, f x < ∑ (x : α) in s, g x

theorem finset.sum_lt_sum_of_nonempty {α : Type u} {β : Type v} {s : finset α} {f g : α → β} [ordered_cancel_add_comm_monoid β] :
s.nonempty(∀ (x : α), x sf x < g x)∑ (x : α) in s, f x < ∑ (x : α) in s, g x

theorem finset.sum_lt_sum_of_subset {α : Type u} {β : Type v} {s₁ s₂ : finset α} {f : α → β} [ordered_cancel_add_comm_monoid β] [decidable_eq α] (h : s₁ s₂) {i : α} :
i s₂ \ s₁0 < f i(∀ (j : α), j s₂ \ s₁0 f j)∑ (x : α) in s₁, f x < ∑ (x : α) in s₂, f x

theorem finset.exists_lt_of_sum_lt {α : Type u} {β : Type v} {s : finset α} {f g : α → β} [linear_ordered_cancel_add_comm_monoid β] :
∑ (x : α) in s, f x < ∑ (x : α) in s, g x(∃ (i : α) (H : i s), f i < g i)

theorem finset.exists_le_of_sum_le {α : Type u} {β : Type v} {s : finset α} {f g : α → β} [linear_ordered_cancel_add_comm_monoid β] :
s.nonempty∑ (x : α) in s, f x ∑ (x : α) in s, g x(∃ (i : α) (H : i s), f i g i)

theorem finset.exists_pos_of_sum_zero_of_exists_nonzero {α : Type u} {β : Type v} {s : finset α} [linear_ordered_cancel_add_comm_monoid β] (f : α → β) :
∑ (e : α) in s, f e = 0(∃ (x : α) (H : x s), f x 0)(∃ (x : α) (H : x s), 0 < f x)

theorem finset.prod_nonneg {α : Type u} {β : Type v} [linear_ordered_comm_ring β] {s : finset α} {f : α → β} :
(∀ (x : α), x s0 f x)0 ∏ (x : α) in s, f x

theorem finset.prod_pos {α : Type u} {β : Type v} [linear_ordered_comm_ring β] {s : finset α} {f : α → β} :
(∀ (x : α), x s0 < f x)0 < ∏ (x : α) in s, f x

theorem finset.prod_le_prod {α : Type u} {β : Type v} [linear_ordered_comm_ring β] {s : finset α} {f g : α → β} :
(∀ (x : α), x s0 f x)(∀ (x : α), x sf x g x)∏ (x : α) in s, f x ∏ (x : α) in s, g x

theorem finset.prod_le_one {α : Type u} {β : Type v} [linear_ordered_comm_ring β] {s : finset α} {f : α → β} :
(∀ (x : α), x s0 f x)(∀ (x : α), x sf x 1)∏ (x : α) in s, f x 1

theorem finset.prod_add_prod_le {α : Type u} {β : Type v} [linear_ordered_comm_ring β] {s : finset α} {i : α} {f g h : α → β} :
i sg i + h i f i(∀ (j : α), j sj ig j f j)(∀ (j : α), j sj ih j f j)(∀ (i : α), i s0 g i)(∀ (i : α), i s0 h i)∏ (i : α) in s, g i + ∏ (i : α) in s, h i ∏ (i : α) in s, 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 linear_ordered_comm_ring.

theorem finset.prod_le_prod' {α : Type u} {β : Type v} [canonically_ordered_comm_semiring β] {s : finset α} {f g : α → β} :
(∀ (i : α), i sf i g i)∏ (x : α) in s, f x ∏ (x : α) in s, g x

theorem finset.prod_add_prod_le' {α : Type u} {β : Type v} [canonically_ordered_comm_semiring β] {s : finset α} {i : α} {f g h : α → β} :
i sg i + h i f i(∀ (j : α), j sj ig j f j)(∀ (j : α), j sj ih j f j)∏ (i : α) in s, g i + ∏ (i : α) in s, h i ∏ (i : α) in s, 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 canonically_ordered_comm_semiring.

theorem with_top.sum_lt_top {α : Type u} {β : Type v} [ordered_add_comm_monoid β] {s : finset α} {f : α → with_top β} :
(∀ (a : α), a sf a < )∑ (x : α) in s, f x <

A sum of finite numbers is still finite

theorem with_top.sum_lt_top_iff {α : Type u} {β : Type v} [canonically_ordered_add_monoid β] {s : finset α} {f : α → with_top β} :
∑ (x : α) in s, f x < ∀ (a : α), a sf a <

A sum of finite numbers is still finite

theorem with_top.sum_eq_top_iff {α : Type u} {β : Type v} [canonically_ordered_add_monoid β] {s : finset α} {f : α → with_top β} :
∑ (x : α) in s, f x = ∃ (a : α) (H : a s), f a =

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

@[simp]
theorem with_top.op_sum {α : Type u} {β : Type v} [add_comm_monoid β] {s : finset α} (f : α → β) :
opposite.op (∑ (x : α) in s, f x) = ∑ (x : α) in s, opposite.op (f x)

Moving to the opposite additive commutative monoid commutes with summing.

@[simp]
theorem with_top.unop_sum {α : Type u} {β : Type v} [add_comm_monoid β] {s : finset α} (f : α → βᵒᵖ) :
opposite.unop (∑ (x : α) in s, f x) = ∑ (x : α) in s, opposite.unop (f x)