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}
[discrete_linear_ordered_field α]
{f : β → α}
{s : finset β} :
theorem
finset.sum_le_sum
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[ordered_add_comm_monoid β]
(a : ∀ (x : α), x ∈ s → f x ≤ g x) :
∑ (x : α) in s, f x ≤ ∑ (x : α) in s, g x
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) :
s.card ≤ n * (finset.image f s).card
theorem
finset.sum_nonneg
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β]
(h : ∀ (x : α), x ∈ s → 0 ≤ 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 ∈ s → f 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) :
theorem
finset.sum_eq_zero_iff_of_nonneg
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β]
(a : ∀ (x : α), x ∈ s → 0 ≤ f x) :
theorem
finset.sum_eq_zero_iff_of_nonpos
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β]
(a : ∀ (x : α), x ∈ s → f x ≤ 0) :
theorem
finset.single_le_sum
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[ordered_add_comm_monoid β]
(hf : ∀ (x : α), x ∈ s → 0 ≤ 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 β] :
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 : α → β) :
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 ≠ 0 → x ∈ 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 ∈ s → f 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 ∈ s → f 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_le_of_sum_le
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[decidable_linear_ordered_cancel_add_comm_monoid β]
(hs : s.nonempty)
(Hle : ∑ (x : α) in s, f x ≤ ∑ (x : α) in s, g x) :
theorem
finset.exists_pos_of_sum_zero_of_exists_nonzero
{α : Type u}
{β : Type v}
{s : finset α}
[decidable_linear_ordered_cancel_add_comm_monoid β]
(f : α → β)
(h₁ : ∑ (e : α) in s, f e = 0)
(h₂ : ∃ (x : α) (H : x ∈ s), f x ≠ 0) :
theorem
finset.prod_nonneg
{α : Type u}
{β : Type v}
[linear_ordered_comm_ring β]
{s : finset α}
{f : α → β}
(h0 : ∀ (x : α), x ∈ s → 0 ≤ 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 ∈ s → 0 < 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 ∈ s → 0 ≤ f x)
(h1 : ∀ (x : α), x ∈ s → f x ≤ g x) :
∏ (x : α) in s, f x ≤ ∏ (x : α) in s, g x
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 ∈ 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) :
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 ∈ s → f 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 ∈ s → j ≠ i → g j ≤ f j)
(hhf : ∀ (j : α), j ∈ s → j ≠ i → h j ≤ f j) :
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 : α), a ∈ s → f a < ⊤) :
A sum of finite numbers is still finite
@[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)