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 : γ → α) :
theorem
finset.abs_sum_le_sum_abs
{α : Type u}
{β : Type v}
[discrete_linear_ordered_field α]
{f : β → α}
{s : finset β} :
theorem
finset.sum_le_sum
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[ordered_add_comm_monoid β] :
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.sum_nonneg
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β] :
theorem
finset.sum_nonpos
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β] :
theorem
finset.sum_mono_set_of_nonneg
{α : Type u}
{β : Type v}
{f : α → β}
[ordered_add_comm_monoid β] :
theorem
finset.single_le_sum
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β]
(hf : ∀ (x : α), x ∈ s → 0 ≤ f x)
{a : α} :
@[simp]
theorem
finset.sum_eq_zero_iff
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[canonically_ordered_add_monoid β] :
theorem
finset.sum_le_sum_of_subset
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[canonically_ordered_add_monoid β] :
theorem
finset.sum_mono_set
{α : Type u}
{β : Type v}
[canonically_ordered_add_monoid β]
(f : α → β) :
theorem
finset.sum_le_sum_of_ne_zero
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[canonically_ordered_add_monoid β] :
theorem
finset.sum_lt_sum_of_nonempty
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[ordered_cancel_add_comm_monoid β] :
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 : α} :
theorem
finset.exists_le_of_sum_le
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[decidable_linear_ordered_cancel_add_comm_monoid β] :
theorem
finset.exists_pos_of_sum_zero_of_exists_nonzero
{α : Type u}
{β : Type v}
{s : finset α}
[decidable_linear_ordered_cancel_add_comm_monoid β]
(f : α → β) :
theorem
finset.prod_nonneg
{α : Type u}
{β : Type v}
[linear_ordered_comm_ring β]
{s : finset α}
{f : α → β} :
theorem
finset.prod_pos
{α : Type u}
{β : Type v}
[linear_ordered_comm_ring β]
{s : finset α}
{f : α → β} :
theorem
finset.prod_le_prod'
{α : Type u}
{β : Type v}
[canonically_ordered_comm_semiring β]
{s : finset α}
{f g : α → β} :
@[simp]
theorem
with_top.op_sum
{α : Type u}
{β : Type v}
[add_comm_monoid β]
{s : finset α}
(f : α → β) :
opposite.op (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), 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 (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), opposite.unop (f x))