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.abs_prod {α : Type u} {β : Type v} [linear_ordered_comm_ring α] {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 : ) (hn : ∀ (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 : ) (hn : ∀ (a : γ), a finset.image f s(finset.filter (λ (x : α), f x = a) s).card n) :

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 : ) (hn : ∀ (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 : ) (hn : ∀ (a : γ), a finset.image f sn (finset.filter (λ (x : α), f x = a) s).card) :

theorem finset.sum_nonneg {α : Type u} {β : Type v} {s : finset α} {f : α → β} [ordered_add_comm_monoid β] (h : ∀ (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 β] (h : ∀ (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 β] (h : s₁ s₂) (hf : ∀ (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 β] (hf : ∀ (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 : α → β} (h : ∀ (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 : α → β} (h : ∀ (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 : α} (h : a s) :
f 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 β] (h : 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 β] (h : ∀ (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 β] (Hle : ∀ (i : α), i sf i g i) (Hlt : ∃ (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 β] (hs : s.nonempty) (Hlt : ∀ (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 : α} (hi : i s₂ \ s₁) (hpos : 0 < f i) (hnonneg : ∀ (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 β] (Hlt : ∑ (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 β] (hs : s.nonempty) (Hle : ∑ (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 : α → β) (h₁ : ∑ (e : α) in s, f e = 0) (h₂ : ∃ (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 : α → β} (h0 : ∀ (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 : α → β} (h0 : ∀ (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 : α → β} (h0 : ∀ (x : α), x s0 f x) (h1 : ∀ (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 : α → β} (h0 : ∀ (x : α), x s0 f x) (h1 : ∀ (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 : α → β} (hi : i s) (h2i : g i + h i f i) (hgf : ∀ (j : α), j sj ig j f j) (hhf : ∀ (j : α), j sj ih j f j) (hg : ∀ (i : α), i s0 g i) (hh : ∀ (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 : α → β} (h : ∀ (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 : α → β} (hi : i s) (h2i : g i + h i f i) (hgf : ∀ (j : α), j sj ig j f j) (hhf : ∀ (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.prod_lt_top {α : Type u} {β : Type v} [canonically_ordered_comm_semiring β] [nontrivial β] [decidable_eq β] {s : finset α} {f : α → with_top β} (h : ∀ (a : α), a sf a < ) :
∏ (x : α) in s, f x <

A product of finite numbers is still finite

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