Module docstring
{"# Big operators on a finset in ordered groups
This file contains the results concerning the interaction of multiset big operators with ordered groups/monoids. "}
Finset.le_prod_nonempty_of_submultiplicative_on_pred
theorem
(f : M → N) (p : M → Prop) (h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ x y, p x → p y → p (x * y))
(g : ι → M) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (g i)) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
Full source
/-- 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 ∈ s, g x) ≤ ∏ x ∈ s, f (g x)`. -/
@[to_additive le_sum_nonempty_of_subadditive_on_pred]
theorem le_prod_nonempty_of_submultiplicative_on_pred (f : M → N) (p : M → Prop)
(h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ x y, p x → p y → p (x * y))
(g : ι → M) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (g i)) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) := by
refine le_trans
(Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_
· simp [hs_nonempty.ne_empty]
· exact Multiset.forall_mem_map_iff.mpr hs
rw [Multiset.map_map]
rflInformal description
Let $M$ and $N$ be ordered commutative monoids, and let $f : M \to N$ be a function that is submultiplicative on a subsemigroup $\{x \in M \mid p(x)\}$, meaning that for any $x, y \in M$ satisfying $p(x)$ and $p(y)$, we have $f(x \cdot y) \leq f(x) \cdot f(y)$. Suppose $\{g_i\}_{i \in s}$ is a nonempty finite family of elements in $M$ such that $p(g_i)$ holds for all $i \in s$. Then, the following inequality holds:
\[ f\left(\prod_{i \in s} g_i\right) \leq \prod_{i \in s} f(g_i). \]
Finset.le_prod_nonempty_of_submultiplicative
theorem
(f : M → N) (h_mul : ∀ x y, f (x * y) ≤ f x * f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
Full source
/-- 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 ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_nonempty_of_subadditive]
theorem le_prod_nonempty_of_submultiplicative (f : M → N) (h_mul : ∀ x y, f (x * y) ≤ f x * f y)
{s : Finset ι} (hs : s.Nonempty) (g : ι → M) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
le_prod_nonempty_of_submultiplicative_on_pred f (fun _ ↦ True) (fun x y _ _ ↦ h_mul x y)
(fun _ _ _ _ ↦ trivial) g s hs fun _ _ ↦ trivialInformal description
Let $M$ and $N$ be ordered commutative monoids, and let $f : M \to N$ be a submultiplicative function, meaning that for all $x, y \in M$, we have $f(x \cdot y) \leq f(x) \cdot f(y)$. For any nonempty finite set $s$ and any family of elements $(g_i)_{i \in s}$ in $M$, the following inequality holds:
\[ f\left(\prod_{i \in s} g_i\right) \leq \prod_{i \in s} f(g_i). \]
Finset.le_prod_of_submultiplicative_on_pred
theorem
(f : M → N) (p : M → Prop) (h_one : f 1 = 1) (h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y)
(hp_mul : ∀ x y, p x → p y → p (x * y)) (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
Full source
/-- 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 ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_of_subadditive_on_pred]
theorem le_prod_of_submultiplicative_on_pred (f : M → N) (p : M → Prop) (h_one : f 1 = 1)
(h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ x y, p x → p y → p (x * y))
(g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) := by
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
· simp [h_one]
· exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hsInformal description
Let $M$ and $N$ be ordered commutative monoids, and let $f : M \to N$ be a function such that $f(1) = 1$. Suppose there exists a predicate $p : M \to \mathrm{Prop}$ defining a subsemigroup of $M$ (i.e., $p(x)$ and $p(y)$ imply $p(x \cdot y)$), and $f$ is submultiplicative on this subsemigroup (i.e., $p(x)$ and $p(y)$ imply $f(x \cdot y) \leq f(x) \cdot f(y)$). For any finite set $s$ and any family of elements $(g_i)_{i \in s}$ in $M$ such that $p(g_i)$ holds for all $i \in s$, we have
\[ f\left(\prod_{i \in s} g_i\right) \leq \prod_{i \in s} f(g_i). \]
Finset.le_prod_of_submultiplicative
theorem
(f : M → N) (h_one : f 1 = 1) (h_mul : ∀ x y, f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
Full source
/-- 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 ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_of_subadditive]
theorem le_prod_of_submultiplicative (f : M → N) (h_one : f 1 = 1)
(h_mul : ∀ x y, f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) := by
refine le_trans (Multiset.le_prod_of_submultiplicative f h_one h_mul _) ?_
rw [Multiset.map_map]
rflInformal description
Let $M$ and $N$ be ordered monoids, and let $f : M \to N$ be a submultiplicative function satisfying $f(1) = 1$ and $f(x \cdot y) \leq f(x) \cdot f(y)$ for all $x, y \in M$. For any finite set $s$ and any family of elements $(g_i)_{i \in s}$ in $M$, we have
\[ f\left(\prod_{i \in s} g_i\right) \leq \prod_{i \in s} f(g_i). \]
Finset.prod_le_prod'
theorem
(h : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
Full source
/-- 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 ∈ s, f i ≤ ∏ i ∈ s, g i`. -/
@[to_additive (attr := gcongr) sum_le_sum]
theorem prod_le_prod' (h : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i :=
Multiset.prod_map_le_prod_map f g hInformal description
Let $s$ be a finite set and let $f, g : \iota \to \alpha$ be functions into an ordered commutative monoid $\alpha$. If for every $i \in s$ we have $f(i) \leq g(i)$, then the product of $f$ over $s$ is less than or equal to the product of $g$ over $s$, i.e.,
\[ \prod_{i \in s} f(i) \leq \prod_{i \in s} g(i). \]
Finset.one_le_prod'
theorem
(h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i
Full source
@[to_additive sum_nonneg]
theorem one_le_prod' (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
le_trans (by rw [prod_const_one]) (prod_le_prod' h)Informal description
Let $s$ be a finite set and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If for every $i \in s$ we have $1 \leq f(i)$, then the product of $f$ over $s$ is greater than or equal to $1$, i.e.,
\[ 1 \leq \prod_{i \in s} f(i). \]
Finset.one_le_prod''
theorem
(h : ∀ i : ι, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i
Full source
@[to_additive Finset.sum_nonneg']
theorem one_le_prod'' (h : ∀ i : ι, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
Finset.one_le_prod' fun i _ ↦ h iInformal description
Let $s$ be a finite set and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If for every $i \in \iota$ we have $1 \leq f(i)$, then the product of $f$ over $s$ is greater than or equal to $1$, i.e.,
\[ 1 \leq \prod_{i \in s} f(i). \]
Finset.prod_le_one'
theorem
(h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1
Full source
@[to_additive sum_nonpos]
theorem prod_le_one' (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
(prod_le_prod' h).trans_eq (by rw [prod_const_one])Informal description
Let $s$ be a finite set and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If for every $i \in s$ we have $f(i) \leq 1$, then the product of $f$ over $s$ is less than or equal to $1$, i.e.,
\[ \prod_{i \in s} f(i) \leq 1. \]
Finset.prod_le_prod_of_subset_of_one_le'
theorem
(h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
Full source
@[to_additive (attr := gcongr) sum_le_sum_of_subset_of_nonneg]
theorem prod_le_prod_of_subset_of_one_le' (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) :
∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
classical calc
∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
_ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
_ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]Informal description
Let $s$ and $t$ be finite sets with $s \subseteq t$, and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If for every $i \in t \setminus s$ we have $1 \leq f(i)$, then the product of $f$ over $s$ is less than or equal to the product of $f$ over $t$, i.e.,
\[ \prod_{i \in s} f(i) \leq \prod_{i \in t} f(i). \]
Finset.prod_mono_set_of_one_le'
theorem
(hf : ∀ x, 1 ≤ f x) : Monotone fun s ↦ ∏ x ∈ s, f x
Full source
@[to_additive sum_mono_set_of_nonneg]
theorem prod_mono_set_of_one_le' (hf : ∀ x, 1 ≤ f x) : Monotone fun s ↦ ∏ x ∈ s, f x :=
fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le' hst fun x _ _ ↦ hf xInformal description
Let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$ such that $1 \leq f(x)$ for all $x \in \iota$. Then the function mapping a finite set $s$ to the product $\prod_{x \in s} f(x)$ is monotone with respect to set inclusion. That is, for any finite sets $s \subseteq t$, we have
\[ \prod_{x \in s} f(x) \leq \prod_{x \in t} f(x). \]
Finset.prod_le_univ_prod_of_one_le'
theorem
[Fintype ι] {s : Finset ι} (w : ∀ x, 1 ≤ f x) : ∏ x ∈ s, f x ≤ ∏ x, f x
Full source
@[to_additive sum_le_univ_sum_of_nonneg]
theorem prod_le_univ_prod_of_one_le' [Fintype ι] {s : Finset ι} (w : ∀ x, 1 ≤ f x) :
∏ x ∈ s, f x ≤ ∏ x, f x :=
prod_le_prod_of_subset_of_one_le' (subset_univ s) fun a _ _ ↦ w aInformal description
Let $\iota$ be a finite type and $s$ be a finite subset of $\iota$. Given a function $f : \iota \to \alpha$ into an ordered commutative monoid $\alpha$ such that $1 \leq f(x)$ for all $x \in \iota$, the product of $f$ over $s$ is less than or equal to the product of $f$ over the entire type $\iota$, i.e.,
\[ \prod_{x \in s} f(x) \leq \prod_{x \in \iota} f(x). \]
Finset.prod_eq_one_iff_of_one_le'
theorem
: (∀ i ∈ s, 1 ≤ f i) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1)
Full source
@[to_additive sum_eq_zero_iff_of_nonneg]
theorem prod_eq_one_iff_of_one_le' :
(∀ i ∈ s, 1 ≤ f i) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := by
classical
refine Finset.induction_on s
(fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
intro a s ha ih H
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
forall_mem_insert, ih this]Informal description
Let $s$ be a finite set and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If $1 \leq f(i)$ for all $i \in s$, then the product of $f$ over $s$ equals $1$ if and only if $f(i) = 1$ for all $i \in s$. In other words,
\[ \prod_{i \in s} f(i) = 1 \leftrightarrow \forall i \in s, f(i) = 1. \]
Finset.prod_eq_one_iff_of_le_one'
theorem
: (∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1)
Full source
@[to_additive sum_eq_zero_iff_of_nonpos]
theorem prod_eq_one_iff_of_le_one' :
(∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) :=
prod_eq_one_iff_of_one_le' (N := Nᵒᵈ)Informal description
Let $s$ be a finite set and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If $f(i) \leq 1$ for all $i \in s$, then the product of $f$ over $s$ equals $1$ if and only if $f(i) = 1$ for all $i \in s$. In other words,
\[ \prod_{i \in s} f(i) = 1 \leftrightarrow \forall i \in s, f(i) = 1. \]
Finset.single_le_prod'
theorem
(hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) : f a ≤ ∏ x ∈ s, f x
Full source
@[to_additive single_le_sum]
theorem single_le_prod' (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) : f a ≤ ∏ x ∈ s, f x :=
calc
f a = ∏ i ∈ {a}, f i := (prod_singleton _ _).symm
_ ≤ ∏ i ∈ s, f i :=
prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) fun i hi _ ↦ hf i hiInformal description
Let $s$ be a finite set and $f : \iota \to \alpha$ a function into an ordered commutative monoid $\alpha$. If $1 \leq f(i)$ for all $i \in s$, then for any element $a \in s$, we have $f(a) \leq \prod_{x \in s} f(x)$.
Finset.mul_le_prod
theorem
{i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) : f i * f j ≤ ∏ k ∈ s, f k
Full source
@[to_additive]
lemma mul_le_prod {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) :
f i * f j ≤ ∏ k ∈ s, f k :=
calc
f i * f j = ∏ k ∈ .cons i {j} (by simpa), f k := by rw [prod_cons, prod_singleton]
_ ≤ ∏ k ∈ s, f k := by
refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk
simp [cons_subset, *]Informal description
Let $s$ be a finite set and $f : \iota \to \alpha$ a function into an ordered commutative monoid $\alpha$. If $1 \leq f(i)$ for all $i \in s$, then for any two distinct elements $i, j \in s$, the product $f(i) \cdot f(j)$ is less than or equal to the product of $f$ over all elements of $s$, i.e.,
\[ f(i) \cdot f(j) \leq \prod_{k \in s} f(k). \]
Finset.prod_le_pow_card
theorem
(s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) : s.prod f ≤ n ^ #s
Full source
@[to_additive sum_le_card_nsmul]
theorem prod_le_pow_card (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
s.prod f ≤ n ^ #s := by
refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_
· simpa using h
· simpInformal description
Let $s$ be a finite set and $f : \iota \to N$ a function from the index type $\iota$ to an ordered monoid $N$. If for every $x \in s$ we have $f(x) \leq n$ for some fixed $n \in N$, then the product of $f$ over $s$ is bounded above by $n$ raised to the power of the cardinality of $s$, i.e.,
\[ \prod_{x \in s} f(x) \leq n^{|s|}. \]
Finset.pow_card_le_prod
theorem
(s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) : n ^ #s ≤ s.prod f
Full source
@[to_additive card_nsmul_le_sum]
theorem pow_card_le_prod (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
n ^ #s ≤ s.prod f := Finset.prod_le_pow_card (N := Nᵒᵈ) _ _ _ hInformal description
Let $s$ be a finite set and $f : \iota \to N$ a function from the index type $\iota$ to an ordered monoid $N$. If for every $x \in s$ we have $n \leq f(x)$ for some fixed $n \in N$, then $n$ raised to the power of the cardinality of $s$ is bounded above by the product of $f$ over $s$, i.e.,
\[ n^{|s|} \leq \prod_{x \in s} f(x). \]
Finset.card_biUnion_le_card_mul
theorem
[DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ) (h : ∀ a ∈ s, #(f a) ≤ n) : #(s.biUnion f) ≤ #s * n
Full source
theorem card_biUnion_le_card_mul [DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ)
(h : ∀ a ∈ s, #(f a) ≤ n) : #(s.biUnion f) ≤ #s * n :=
card_biUnion_le.trans <| sum_le_card_nsmul _ _ _ hInformal description
Let $s$ be a finite set indexed by $\iota$, and for each $a \in s$, let $f(a)$ be a finite subset of $\beta$. If for every $a \in s$ the cardinality of $f(a)$ is at most $n$, then the cardinality of the union $\bigcup_{a \in s} f(a)$ is at most the product of the cardinality of $s$ and $n$, i.e.,
\[ \left|\bigcup_{a \in s} f(a)\right| \leq |s| \cdot n. \]
Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'
theorem
{t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, (1 : N) ≤ ∏ x ∈ s with g x = y, f x) :
(∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤ ∏ x ∈ s, f x
Full source
@[to_additive sum_fiberwise_le_sum_of_sum_fiber_nonneg]
theorem prod_fiberwise_le_prod_of_one_le_prod_fiber' {t : Finset ι'} {g : ι → ι'} {f : ι → N}
(h : ∀ y ∉ t, (1 : N) ≤ ∏ x ∈ s with g x = y, f x) :
(∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤ ∏ x ∈ s, f x :=
calc
(∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤
∏ y ∈ t ∪ s.image g, ∏ x ∈ s with g x = y, f x :=
prod_le_prod_of_subset_of_one_le' subset_union_left fun y _ ↦ h y
_ = ∏ x ∈ s, f x :=
prod_fiberwise_of_maps_to (fun _ hx ↦ mem_union.2 <| Or.inr <| mem_image_of_mem _ hx) _Informal description
Let $s$ be a finite set indexed by $\iota$, $t$ a finite set indexed by $\iota'$, $g : \iota \to \iota'$ a function, and $f : \iota \to N$ a function into an ordered commutative monoid $N$. If for every $y \notin t$ the product of $f(x)$ over all $x \in s$ with $g(x) = y$ is at least $1$, then the product over $t$ of the products of $f(x)$ over the fibers $g^{-1}(y) \cap s$ is less than or equal to the product of $f(x)$ over $s$, i.e.,
\[ \prod_{y \in t} \prod_{\substack{x \in s \\ g(x) = y}} f(x) \leq \prod_{x \in s} f(x). \]
Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one'
theorem
{t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) :
∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x
Full source
@[to_additive sum_le_sum_fiberwise_of_sum_fiber_nonpos]
theorem prod_le_prod_fiberwise_of_prod_fiber_le_one' {t : Finset ι'} {g : ι → ι'} {f : ι → N}
(h : ∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) :
∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x :=
prod_fiberwise_le_prod_of_one_le_prod_fiber' (N := Nᵒᵈ) hInformal description
Let $s$ be a finite set indexed by $\iota$, $t$ a finite set indexed by $\iota'$, $g : \iota \to \iota'$ a function, and $f : \iota \to N$ a function into an ordered commutative monoid $N$. If for every $y \notin t$ the product of $f(x)$ over all $x \in s$ with $g(x) = y$ is at most $1$, then the product of $f(x)$ over $s$ is less than or equal to the product over $t$ of the products of $f(x)$ over the fibers $g^{-1}(y) \cap s$, i.e.,
\[ \prod_{x \in s} f(x) \leq \prod_{y \in t} \prod_{\substack{x \in s \\ g(x) = y}} f(x). \]
Finset.prod_image_le_of_one_le
theorem
{g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ s.image g, 1 ≤ f u) : ∏ u ∈ s.image g, f u ≤ ∏ u ∈ s, f (g u)
Full source
@[to_additive]
lemma prod_image_le_of_one_le
{g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ s.image g, 1 ≤ f u) :
∏ u ∈ s.image g, f u ≤ ∏ u ∈ s, f (g u) := by
rw [prod_comp f g]
refine prod_le_prod' fun a hag ↦ ?_
obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag
apply le_self_pow (hf a hag)
rw [← Nat.pos_iff_ne_zero, card_pos]
exact ⟨i, mem_filter.mpr ⟨hi, hig⟩⟩Informal description
Let $s$ be a finite set, $g : \iota \to \iota'$ a function, and $f : \iota' \to N$ a function into an ordered commutative monoid $N$. If for every $u$ in the image of $g$ over $s$ we have $1 \leq f(u)$, then the product of $f$ over the image of $g$ is less than or equal to the product of $f \circ g$ over $s$, i.e.,
\[ \prod_{u \in g(s)} f(u) \leq \prod_{u \in s} f(g(u)). \]
Finset.max_prod_le
theorem
[CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
max (s.prod f) (s.prod g) ≤ s.prod (fun i ↦ max (f i) (g i))
Full source
@[to_additive]
lemma max_prod_le [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
max (s.prod f) (s.prod g) ≤ s.prod (fun i ↦ max (f i) (g i)) :=
Multiset.max_prod_leInformal description
Let $M$ be a linearly ordered commutative monoid, $s$ a finite set, and $f, g : \iota \to M$ two functions. Then the maximum of the products of $f$ and $g$ over $s$ is less than or equal to the product over $s$ of the pointwise maxima of $f$ and $g$, i.e.,
\[ \max\left(\prod_{i \in s} f(i), \prod_{i \in s} g(i)\right) \leq \prod_{i \in s} \max(f(i), g(i)). \]
Finset.prod_min_le
theorem
[CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
s.prod (fun i ↦ min (f i) (g i)) ≤ min (s.prod f) (s.prod g)
Full source
@[to_additive]
lemma prod_min_le [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
s.prod (fun i ↦ min (f i) (g i)) ≤ min (s.prod f) (s.prod g) :=
Multiset.prod_min_leInformal description
Let $M$ be a linearly ordered commutative monoid, and let $f, g : \iota \to M$ be functions. For any finite set $s \subset \iota$, the product of the pointwise minima $\min(f(i), g(i))$ over $s$ is less than or equal to the minimum of the products of $f$ and $g$ over $s$. That is,
\[ \prod_{i \in s} \min(f(i), g(i)) \leq \min\left(\prod_{i \in s} f(i), \prod_{i \in s} g(i)\right). \]
Finset.abs_sum_le_sum_abs
theorem
{G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (f : ι → G) (s : Finset ι) :
|∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i|
Full source
theorem abs_sum_le_sum_abs {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
(f : ι → G) (s : Finset ι) :
|∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i| := le_sum_of_subadditive _ abs_zero abs_add s fInformal description
Let $G$ be an additively commutative group with a linear order and an ordered additive monoid structure. For any function $f : \iota \to G$ and any finite set $s \subseteq \iota$, the absolute value of the sum of $f$ over $s$ is less than or equal to the sum of the absolute values of $f$ over $s$, i.e.,
$$
\left| \sum_{i \in s} f(i) \right| \leq \sum_{i \in s} |f(i)|.
$$
Finset.abs_sum_of_nonneg
theorem
{G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {f : ι → G} {s : Finset ι}
(hf : ∀ i ∈ s, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i
Full source
theorem abs_sum_of_nonneg {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
{f : ι → G} {s : Finset ι}
(hf : ∀ i ∈ s, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by
rw [abs_of_nonneg (Finset.sum_nonneg hf)]Informal description
Let $G$ be an ordered additive commutative group with a linear order and an ordered additive monoid structure. For any function $f : \iota \to G$ and finite set $s \subseteq \iota$, if $f(i) \geq 0$ for all $i \in s$, then the absolute value of the sum of $f$ over $s$ equals the sum of $f$ over $s$, i.e., $\left|\sum_{i \in s} f(i)\right| = \sum_{i \in s} f(i)$.
Finset.abs_sum_of_nonneg'
theorem
{G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {f : ι → G} {s : Finset ι} (hf : ∀ i, 0 ≤ f i) :
|∑ i ∈ s, f i| = ∑ i ∈ s, f i
Full source
theorem abs_sum_of_nonneg' {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
{f : ι → G} {s : Finset ι}
(hf : ∀ i, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by
rw [abs_of_nonneg (Finset.sum_nonneg' hf)]Informal description
Let $G$ be an additively commutative group with a linear order and an ordered additive monoid structure. For any function $f : \iota \to G$ and any finite set $s \subseteq \iota$, if $f(i) \geq 0$ for all $i \in \iota$, then the absolute value of the sum $\sum_{i \in s} f(i)$ is equal to the sum $\sum_{i \in s} f(i)$.
Finset.mulLECancellable_prod
theorem
: MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i⦄, i ∈ s → MulLECancellable (f i)
Full source
@[to_additive (attr := simp)]
lemma mulLECancellable_prod :
MulLECancellableMulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i⦄, i ∈ s → MulLECancellable (f i) := by
induction' s using Finset.cons_induction with i s hi ih <;> simp [*]Informal description
For a finite set $s$ and a function $f$ defined on $s$, the product $\prod_{i \in s} f(i)$ is multiplicatively cancellable (i.e., $a \cdot b \leq a \cdot c$ implies $b \leq c$ for any $a, b, c$) if and only if for every $i \in s$, the element $f(i)$ is multiplicatively cancellable.
Finset.card_le_mul_card_image_of_maps_to
theorem
{f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, #({a ∈ s | f a = b}) ≤ n) :
#s ≤ n * #t
Full source
theorem card_le_mul_card_image_of_maps_to {f : α → β} {s : Finset α} {t : Finset β}
(Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, #{a ∈ s | f a = b} ≤ n) : #s ≤ n * #t :=
calc
#s = ∑ b ∈ t, #{a ∈ s | f a = b} := card_eq_sum_card_fiberwise Hf
_ ≤ ∑ _b ∈ t, n := sum_le_sum hn
_ = _ := by simp [mul_comm]Informal description
Let $f : \alpha \to \beta$ be a function, $s$ a finite subset of $\alpha$, and $t$ a finite subset of $\beta$ such that for every $a \in s$, $f(a) \in t$. If there exists a natural number $n$ such that for every $b \in t$, the number of elements $a \in s$ with $f(a) = b$ is at most $n$, then $|s| \leq n \cdot |t|$.
Finset.card_le_mul_card_image
theorem
{f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ b ∈ s.image f, #({a ∈ s | f a = b}) ≤ n) : #s ≤ n * #(s.image f)
Full source
theorem card_le_mul_card_image {f : α → β} (s : Finset α) (n : ℕ)
(hn : ∀ b ∈ s.image f, #{a ∈ s | f a = b} ≤ n) : #s ≤ n * #(s.image f) :=
card_le_mul_card_image_of_maps_to (fun _ ↦ mem_image_of_mem _) n hnInformal description
Let $f : \alpha \to \beta$ be a function and $s$ a finite subset of $\alpha$. If there exists a natural number $n$ such that for every $b$ in the image of $f$ on $s$, the number of elements $a \in s$ with $f(a) = b$ is at most $n$, then the cardinality of $s$ satisfies $|s| \leq n \cdot |f(s)|$.
Finset.mul_card_image_le_card_of_maps_to
theorem
{f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})) :
n * #t ≤ #s
Full source
theorem mul_card_image_le_card_of_maps_to {f : α → β} {s : Finset α} {t : Finset β}
(Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, n ≤ #{a ∈ s | f a = b}) :
n * #t ≤ #s :=
calc
n * #t = ∑ _a ∈ t, n := by simp [mul_comm]
_ ≤ ∑ b ∈ t, #{a ∈ s | f a = b} := sum_le_sum hn
_ = #s := by rw [← card_eq_sum_card_fiberwise Hf]Informal description
Let $f : \alpha \to \beta$ be a function, $s$ a finite subset of $\alpha$, and $t$ a finite subset of $\beta$ such that for every $a \in s$, $f(a) \in t$. If there exists a natural number $n$ such that for every $b \in t$, the number of elements $a \in s$ with $f(a) = b$ is at least $n$, then $n \cdot |t| \leq |s|$.
Finset.mul_card_image_le_card
theorem
{f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ b ∈ s.image f, n ≤ #({a ∈ s | f a = b})) : n * #(s.image f) ≤ #s
Full source
theorem mul_card_image_le_card {f : α → β} (s : Finset α) (n : ℕ)
(hn : ∀ b ∈ s.image f, n ≤ #{a ∈ s | f a = b}) : n * #(s.image f) ≤ #s :=
mul_card_image_le_card_of_maps_to (fun _ ↦ mem_image_of_mem _) n hnInformal description
Let $f : \alpha \to \beta$ be a function and $s$ a finite subset of $\alpha$. If there exists a natural number $n$ such that for every $b$ in the image $f(s)$, the number of elements $a \in s$ with $f(a) = b$ is at least $n$, then $n \cdot |f(s)| \leq |s|$.
Finset.sum_card_inter_le
theorem
(h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n) : (∑ t ∈ B, #(s ∩ t)) ≤ #s * n
Full source
/-- 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 sum_card_inter_le (h : ∀ a ∈ s, #{b ∈ B | a ∈ b} ≤ n) : (∑ t ∈ B, #(s ∩ t)) ≤ #s * n := by
refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
exact sum_comm.leInformal description
Let $s$ be a finite set and $B$ a finite family of sets. If for every element $a \in s$, the number of sets in $B$ containing $a$ is at most $n$, then the sum of the cardinalities of the intersections of $s$ with each set in $B$ is at most $|s| \cdot n$. In other words,
\[ \sum_{t \in B} |s \cap t| \leq |s| \cdot n. \]
Finset.sum_card_le
theorem
[Fintype α] (h : ∀ a, #({b ∈ B | a ∈ b}) ≤ n) : ∑ s ∈ B, #s ≤ Fintype.card α * n
Full source
/-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
times how many they are. -/
lemma sum_card_le [Fintype α] (h : ∀ a, #{b ∈ B | a ∈ b} ≤ n) : ∑ s ∈ B, #s ≤ Fintype.card α * n :=
calc
∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s) := by simp_rw [univ_inter]
_ ≤ Fintype.card α * n := sum_card_inter_le fun a _ ↦ h aInformal description
Let $\alpha$ be a finite type and $B$ a finite family of subsets of $\alpha$. If for every element $a \in \alpha$, the number of sets in $B$ containing $a$ is at most $n$, then the sum of the cardinalities of all sets in $B$ is at most $|\alpha| \cdot n$. In other words,
\[ \sum_{s \in B} |s| \leq |\alpha| \cdot n. \]
Finset.le_sum_card_inter
theorem
(h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})) : #s * n ≤ ∑ t ∈ B, #(s ∩ t)
Full source
/-- 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 le_sum_card_inter (h : ∀ a ∈ s, n ≤ #{b ∈ B | a ∈ b}) : #s * n ≤ ∑ t ∈ B, #(s ∩ t) := by
apply (s.card_nsmul_le_sum _ _ h).trans
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
exact sum_comm.leInformal description
Let $s$ be a finite set and $B$ a finite family of sets. If for every element $a \in s$, the number of sets in $B$ containing $a$ is at least $n$, then the sum of the cardinalities of the intersections of $s$ with each set in $B$ is at least $|s| \cdot n$. In other words,
\[ |s| \cdot n \leq \sum_{t \in B} |s \cap t|. \]
Finset.le_sum_card
theorem
[Fintype α] (h : ∀ a, n ≤ #({b ∈ B | a ∈ b})) : Fintype.card α * n ≤ ∑ s ∈ B, #s
Full source
/-- 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 le_sum_card [Fintype α] (h : ∀ a, n ≤ #{b ∈ B | a ∈ b}) :
Fintype.card α * n ≤ ∑ s ∈ B, #s :=
calc
Fintype.card α * n ≤ ∑ s ∈ B, #(univ ∩ s) := le_sum_card_inter fun a _ ↦ h a
_ = ∑ s ∈ B, #s := by simp_rw [univ_inter]Informal description
Let $\alpha$ be a finite type and $B$ a finite family of subsets of $\alpha$. If for every element $a \in \alpha$, the number of sets in $B$ containing $a$ is at least $n$, then the sum of the cardinalities of all sets in $B$ is at least $|\alpha| \cdot n$. In other words,
\[ |\alpha| \cdot n \leq \sum_{s \in B} |s|. \]
Finset.sum_card_inter
theorem
(h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) = n) : (∑ t ∈ B, #(s ∩ t)) = #s * n
Full source
/-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
many they are. -/
theorem sum_card_inter (h : ∀ a ∈ s, #{b ∈ B | a ∈ b} = n) :
(∑ t ∈ B, #(s ∩ t)) = #s * n :=
(sum_card_inter_le fun a ha ↦ (h a ha).le).antisymm (le_sum_card_inter fun a ha ↦ (h a ha).ge)Informal description
Let $s$ be a finite set and $B$ a finite family of sets. If for every element $a \in s$, the number of sets in $B$ containing $a$ is exactly $n$, then the sum of the cardinalities of the intersections of $s$ with each set in $B$ equals $|s| \cdot n$. In other words,
\[ \sum_{t \in B} |s \cap t| = |s| \cdot n. \]
Finset.sum_card
theorem
[Fintype α] (h : ∀ a, #({b ∈ B | a ∈ b}) = n) : ∑ s ∈ B, #s = Fintype.card α * n
Full source
/-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
many they are. -/
theorem sum_card [Fintype α] (h : ∀ a, #{b ∈ B | a ∈ b} = n) :
∑ s ∈ B, #s = Fintype.card α * n := by
simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]Informal description
Let $\alpha$ be a finite type and $B$ a finite family of subsets of $\alpha$. If for every element $a \in \alpha$, the number of sets in $B$ containing $a$ is exactly $n$, then the sum of the cardinalities of all sets in $B$ equals $|\alpha| \cdot n$. In other words,
\[ \sum_{s \in B} |s| = |\alpha| \cdot n. \]
Finset.card_le_card_biUnion
theorem
{s : Finset ι} {f : ι → Finset α} (hs : (s : Set ι).PairwiseDisjoint f) (hf : ∀ i ∈ s, (f i).Nonempty) :
#s ≤ #(s.biUnion f)
Full source
theorem card_le_card_biUnion {s : Finset ι} {f : ι → Finset α} (hs : (s : Set ι).PairwiseDisjoint f)
(hf : ∀ i ∈ s, (f i).Nonempty) : #s ≤ #(s.biUnion f) := by
rw [card_biUnion hs, card_eq_sum_ones]
exact sum_le_sum fun i hi ↦ (hf i hi).card_posInformal description
Let $s$ be a finite set of indices of type $\iota$, and let $f \colon \iota \to \text{Finset } \alpha$ be a function assigning to each index a finite subset of $\alpha$. If:
1. The images of $f$ are pairwise disjoint (i.e., for any distinct $i, j \in s$, $f(i) \cap f(j) = \emptyset$), and
2. For every $i \in s$, the set $f(i)$ is nonempty,
then the cardinality of $s$ is less than or equal to the cardinality of the union $\bigcup_{i \in s} f(i)$.
In mathematical notation:
$$|s| \leq \left|\bigcup_{i \in s} f(i)\right|$$
Finset.card_le_card_biUnion_add_card_fiber
theorem
{s : Finset ι} {f : ι → Finset α} (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Full source
theorem card_le_card_biUnion_add_card_fiber {s : Finset ι} {f : ι → Finset α}
(hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + #{i ∈ s | f i = ∅} := by
rw [← Finset.filter_card_add_filter_neg_card_eq_card fun i ↦ f i = ∅, add_comm]
exact
add_le_add_right
((card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
nonempty_of_ne_empty <| (mem_filter.1 hi).2).trans <|
card_le_card <| biUnion_subset_biUnion_of_subset_left _ <| filter_subset _ _)
_Informal description
Let $s$ be a finite set of indices of type $\iota$, and let $f \colon \iota \to \text{Finset } \alpha$ be a function assigning to each index a finite subset of $\alpha$. If the images of $f$ are pairwise disjoint (i.e., for any distinct $i, j \in s$, $f(i) \cap f(j) = \emptyset$), then the cardinality of $s$ is less than or equal to the sum of the cardinality of the union $\bigcup_{i \in s} f(i)$ and the number of indices $i \in s$ for which $f(i)$ is empty.
In mathematical notation:
$$|s| \leq \left|\bigcup_{i \in s} f(i)\right| + \left|\{i \in s \mid f(i) = \emptyset\}\right|$$
Finset.card_le_card_biUnion_add_one
theorem
{s : Finset ι} {f : ι → Finset α} (hf : Injective f) (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + 1
Full source
theorem card_le_card_biUnion_add_one {s : Finset ι} {f : ι → Finset α} (hf : Injective f)
(hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + 1 :=
(card_le_card_biUnion_add_card_fiber hs).trans <|
add_le_add_left
(card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm) _Informal description
Let $s$ be a finite set of indices of type $\iota$, and let $f \colon \iota \to \text{Finset } \alpha$ be an injective function assigning to each index a finite subset of $\alpha$. If the images of $f$ are pairwise disjoint (i.e., for any distinct $i, j \in s$, $f(i) \cap f(j) = \emptyset$), then the cardinality of $s$ is less than or equal to the cardinality of the union $\bigcup_{i \in s} f(i)$ plus one.
In mathematical notation:
$$|s| \leq \left|\bigcup_{i \in s} f(i)\right| + 1$$
CanonicallyOrderedCommMonoid.single_le_prod
theorem
{i : ι} (hi : i ∈ s) : f i ≤ ∏ j ∈ s, f j
Full source
/-- In a canonically-ordered monoid, a product bounds each of its terms.
See also `Finset.single_le_prod'`. -/
@[to_additive "In a canonically-ordered additive monoid, a sum bounds each of its terms.
See also `Finset.single_le_sum`."]
lemma _root_.CanonicallyOrderedCommMonoid.single_le_prod {i : ι} (hi : i ∈ s) :
f i ≤ ∏ j ∈ s, f j :=
single_le_prod' (fun _ _ ↦ one_le _) hiInformal description
Let $s$ be a finite set and $f \colon \iota \to \alpha$ a function into a canonically ordered commutative monoid $\alpha$. For any element $i \in s$, the value $f(i)$ is less than or equal to the product $\prod_{j \in s} f(j)$.
Finset.prod_le_prod_of_subset'
theorem
(h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
Full source
@[to_additive sum_le_sum_of_subset]
theorem prod_le_prod_of_subset' (h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x :=
prod_le_prod_of_subset_of_one_le' h fun _ _ _ ↦ one_le _Informal description
For any finite sets $s$ and $t$ with $s \subseteq t$, and any function $f : \iota \to \alpha$ into an ordered commutative monoid $\alpha$, the product of $f$ over $s$ is less than or equal to the product of $f$ over $t$, i.e.,
\[ \prod_{x \in s} f(x) \leq \prod_{x \in t} f(x). \]
Finset.prod_mono_set'
theorem
(f : ι → M) : Monotone fun s ↦ ∏ x ∈ s, f x
Full source
@[to_additive sum_mono_set]
theorem prod_mono_set' (f : ι → M) : Monotone fun s ↦ ∏ x ∈ s, f x := fun _ _ hs ↦
prod_le_prod_of_subset' hsInformal description
For any function $f \colon \iota \to M$ into an ordered commutative monoid $M$, the map sending a finite set $s$ to the product $\prod_{x \in s} f(x)$ is monotone with respect to set inclusion. That is, if $s \subseteq t$ are finite sets, then $\prod_{x \in s} f(x) \leq \prod_{x \in t} f(x)$.
Finset.prod_le_prod_of_ne_one'
theorem
(h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
Full source
@[to_additive sum_le_sum_of_ne_zero]
theorem prod_le_prod_of_ne_one' (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
∏ x ∈ s, f x ≤ ∏ x ∈ t, f x := by
classical calc
∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
rw [← prod_union, filter_union_filter_neg_eq]
exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
_ ≤ ∏ x ∈ t, f x :=
mul_le_of_le_one_of_le
(prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
(prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp] )Informal description
Let $s$ and $t$ be finite sets, and let $f : \iota \to \alpha$ be a function into an ordered commutative monoid $\alpha$. If for every $x \in s$ with $f(x) \neq 1$ we have $x \in t$, then the product of $f$ over $s$ is less than or equal to the product of $f$ over $t$, i.e.,
\[ \prod_{x \in s} f(x) \leq \prod_{x \in t} f(x). \]
Finset.prod_lt_prod'
theorem
(hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : ∏ i ∈ s, f i < ∏ i ∈ s, g i
Full source
@[to_additive sum_lt_sum]
theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i :=
Multiset.prod_lt_prod' hle hltInformal description
Let $s$ be a finite set and $f, g$ be functions from a type $\iota$ to an ordered cancellative monoid $M$. If for every $i \in s$ we have $f(i) \leq g(i)$, and there exists some $i \in s$ such that $f(i) < g(i)$, then the product of $f$ over $s$ is strictly less than the product of $g$ over $s$, i.e., $\prod_{i \in s} f(i) < \prod_{i \in s} g(i)$.
Finset.prod_lt_prod_of_nonempty'
theorem
(hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) : ∏ i ∈ s, f i < ∏ i ∈ s, g i
Full source
/-- 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`. -/
@[to_additive (attr := gcongr) sum_lt_sum_of_nonempty]
theorem prod_lt_prod_of_nonempty' (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i :=
Multiset.prod_lt_prod_of_nonempty' (by aesop) hltInformal description
Let $s$ be a nonempty finite set and let $f, g$ be functions from a type $\iota$ to an ordered cancellative monoid $M$. If for every $i \in s$ we have $f(i) < g(i)$, then the product of $f$ over $s$ is strictly less than the product of $g$ over $s$, i.e., $\prod_{i \in s} f(i) < \prod_{i \in s} g(i)$.
Finset.prod_lt_prod_of_subset'
theorem
(h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i) (hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) :
∏ j ∈ s, f j < ∏ j ∈ t, f j
Full source
@[to_additive sum_lt_sum_of_subset]
theorem prod_lt_prod_of_subset' (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i)
(hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) : ∏ j ∈ s, f j < ∏ j ∈ t, f j := by
classical calc
∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
rw [prod_insert hs]
exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
_ ≤ ∏ j ∈ t, f j := by
apply prod_le_prod_of_subset_of_one_le'
· simp [Finset.insert_subset_iff, h, ht]
· intro x hx h'x
simp only [mem_insert, not_or] at h'x
exact hle x hx h'x.2Informal description
Let $s$ and $t$ be finite sets with $s \subseteq t$, and let $f : \iota \to \alpha$ be a function into an ordered cancellative monoid $\alpha$. Suppose there exists an element $i \in t \setminus s$ such that $1 < f(i)$, and for all other elements $j \in t \setminus s$ we have $1 \leq f(j)$. Then the product of $f$ over $s$ is strictly less than the product of $f$ over $t$, i.e.,
\[ \prod_{j \in s} f(j) < \prod_{j \in t} f(j). \]
Finset.single_lt_prod'
theorem
{i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j) (hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) : f i < ∏ k ∈ s, f k
Full source
@[to_additive single_lt_sum]
theorem single_lt_prod' {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j)
(hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) : f i < ∏ k ∈ s, f k :=
calc
f i = ∏ k ∈ {i}, f k := by rw [prod_singleton]
_ < ∏ k ∈ s, f k :=
prod_lt_prod_of_subset' (singleton_subset_iff.2 hi) hj (mt mem_singleton.1 hij) hlt
fun k hks hki ↦ hle k hks (mt mem_singleton.2 hki)Informal description
Let $s$ be a finite set and let $f : \iota \to \alpha$ be a function into an ordered cancellative monoid $\alpha$. For any two distinct elements $i, j \in s$ such that $1 < f(j)$ and for all other elements $k \in s \setminus \{i\}$ we have $1 \leq f(k)$, the value of $f$ at $i$ is strictly less than the product of $f$ over $s$, i.e.,
\[ f(i) < \prod_{k \in s} f(k). \]
Finset.one_lt_prod
theorem
(h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) : 1 < ∏ i ∈ s, f i
Full source
@[to_additive sum_pos]
theorem one_lt_prod (h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) : 1 < ∏ i ∈ s, f i :=
lt_of_le_of_lt (by rw [prod_const_one]) <| prod_lt_prod_of_nonempty' hs hInformal description
Let $s$ be a nonempty finite set and let $f$ be a function from a type $\iota$ to an ordered cancellative monoid $M$. If for every $i \in s$ we have $1 < f(i)$, then the product of $f$ over $s$ is strictly greater than $1$, i.e., $\prod_{i \in s} f(i) > 1$.
Finset.prod_lt_one
theorem
(h : ∀ i ∈ s, f i < 1) (hs : s.Nonempty) : ∏ i ∈ s, f i < 1
Full source
@[to_additive]
theorem prod_lt_one (h : ∀ i ∈ s, f i < 1) (hs : s.Nonempty) : ∏ i ∈ s, f i < 1 :=
(prod_lt_prod_of_nonempty' hs h).trans_le (by rw [prod_const_one])Informal description
Let $s$ be a nonempty finite set and let $f$ be a function from a type $\iota$ to an ordered cancellative monoid $M$. If for every $i \in s$ we have $f(i) < 1$, then the product of $f$ over $s$ is strictly less than $1$, i.e., $\prod_{i \in s} f(i) < 1$.
Finset.one_lt_prod'
theorem
(h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) : 1 < ∏ i ∈ s, f i
Full source
@[to_additive sum_pos']
theorem one_lt_prod' (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) : 1 < ∏ i ∈ s, f i :=
prod_const_one.symm.trans_lt <| prod_lt_prod' h hsInformal description
Let $s$ be a finite set and $f : \iota \to M$ be a function into an ordered cancellative monoid $M$. If $f(i) \geq 1$ for all $i \in s$, and there exists some $i \in s$ such that $f(i) > 1$, then the product of $f$ over $s$ is strictly greater than $1$, i.e., $\prod_{i \in s} f(i) > 1$.
Finset.prod_lt_one'
theorem
(h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) : ∏ i ∈ s, f i < 1
Full source
@[to_additive]
theorem prod_lt_one' (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) : ∏ i ∈ s, f i < 1 :=
prod_const_one.le.trans_lt' <| prod_lt_prod' h hsInformal description
Let $s$ be a finite set and $f : \iota \to M$ be a function into an ordered cancellative monoid $M$. If $f(i) \leq 1$ for all $i \in s$, and there exists some $i \in s$ such that $f(i) < 1$, then the product of $f$ over $s$ is strictly less than $1$, i.e., $\prod_{i \in s} f(i) < 1$.
Finset.prod_eq_prod_iff_of_le
theorem
{f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) : ((∏ i ∈ s, f i) = ∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
Full source
@[to_additive]
theorem prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
((∏ i ∈ s, f i) = ∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i := by
classical
revert h
refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h),
fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
exact
mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a))
(Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)Informal description
Let $s$ be a finite set and $f, g : \iota \to M$ be functions into an ordered cancellative monoid $M$. If $f(i) \leq g(i)$ for all $i \in s$, then the product of $f$ over $s$ equals the product of $g$ over $s$ if and only if $f(i) = g(i)$ for all $i \in s$. In other words,
\[ \prod_{i \in s} f(i) = \prod_{i \in s} g(i) \leftrightarrow \forall i \in s, f(i) = g(i). \]
Finset.prod_sdiff_le_prod_sdiff
theorem
: ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
Full source
@[to_additive] lemma prod_sdiff_le_prod_sdiff :
∏ i ∈ s \ t, f i∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
← prod_union, inter_comm, sdiff_union_inter]
simpa only [inter_comm] using disjoint_sdiff_inter t sInformal description
Let $M$ be an ordered cancellative monoid, $s$ and $t$ be finite sets, and $f : \iota \to M$ be a function. Then the product of $f$ over the symmetric difference $s \setminus t$ is less than or equal to the product over $t \setminus s$ if and only if the product over $s$ is less than or equal to the product over $t$. In other words,
\[ \prod_{i \in s \setminus t} f(i) \leq \prod_{i \in t \setminus s} f(i) \leftrightarrow \prod_{i \in s} f(i) \leq \prod_{i \in t} f(i). \]
Finset.prod_sdiff_lt_prod_sdiff
theorem
: ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i
Full source
@[to_additive] lemma prod_sdiff_lt_prod_sdiff :
∏ i ∈ s \ t, f i∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i := by
rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
← prod_union, inter_comm, sdiff_union_inter]
simpa only [inter_comm] using disjoint_sdiff_inter t sInformal description
Let $M$ be an ordered cancellative monoid, $s$ and $t$ be finite sets, and $f : \iota \to M$ be a function. Then the product of $f$ over the symmetric difference $s \setminus t$ is strictly less than the product over $t \setminus s$ if and only if the product over $s$ is strictly less than the product over $t$. In other words,
\[ \prod_{i \in s \setminus t} f(i) < \prod_{i \in t \setminus s} f(i) \leftrightarrow \prod_{i \in s} f(i) < \prod_{i \in t} f(i). \]
Finset.exists_lt_of_prod_lt'
theorem
(Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) : ∃ i ∈ s, f i < g i
Full source
@[to_additive exists_lt_of_sum_lt]
theorem exists_lt_of_prod_lt' (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) : ∃ i ∈ s, f i < g i := by
contrapose! Hlt with Hle
exact prod_le_prod' HleInformal description
Let $s$ be a finite set and let $f, g : \iota \to M$ be functions into an ordered cancellative monoid $M$. If the product of $f$ over $s$ is strictly less than the product of $g$ over $s$, i.e.,
\[ \prod_{i \in s} f(i) < \prod_{i \in s} g(i), \]
then there exists an element $i \in s$ such that $f(i) < g(i)$.
Finset.exists_le_of_prod_le'
theorem
(hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i
Full source
@[to_additive exists_le_of_sum_le]
theorem exists_le_of_prod_le' (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) :
∃ i ∈ s, f i ≤ g i := by
contrapose! Hle with Hlt
exact prod_lt_prod_of_nonempty' hs HltInformal description
Let $s$ be a nonempty finite set and let $f, g$ be functions from a type $\iota$ to an ordered cancellative monoid $M$. If the product of $f$ over $s$ is less than or equal to the product of $g$ over $s$, i.e., $\prod_{i \in s} f(i) \leq \prod_{i \in s} g(i)$, then there exists an element $i \in s$ such that $f(i) \leq g(i)$.
Finset.exists_one_lt_of_prod_one_of_exists_ne_one'
theorem
(f : ι → M) (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i
Full source
@[to_additive exists_pos_of_sum_zero_of_exists_nonzero]
theorem exists_one_lt_of_prod_one_of_exists_ne_one' (f : ι → M) (h₁ : ∏ i ∈ s, f i = 1)
(h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i := by
contrapose! h₁
obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
apply ne_of_lt
calc
∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
_ = 1 := prod_const_oneInformal description
Let $s$ be a finite set, $M$ an ordered cancellative monoid, and $f : \iota \to M$ a function. If the product of $f$ over $s$ equals $1$ and there exists some $i \in s$ such that $f(i) \neq 1$, then there exists some $i \in s$ such that $1 < f(i)$.
Fintype.prod_mono'
theorem
: Monotone fun f : ι → M ↦ ∏ i, f i
Full source
@[to_additive (attr := mono) sum_mono]
theorem prod_mono' : Monotone fun f : ι → M ↦ ∏ i, f i := fun _ _ hfg ↦
Finset.prod_le_prod' fun x _ ↦ hfg xInformal description
For any finite type $\iota$ and any ordered commutative monoid $M$, the product function $\prod_{i \in \iota} f(i)$ is monotone. That is, if $f, g : \iota \to M$ satisfy $f(i) \leq g(i)$ for all $i \in \iota$, then
\[ \prod_{i \in \iota} f(i) \leq \prod_{i \in \iota} g(i). \]
Fintype.one_le_prod
theorem
(hf : 1 ≤ f) : 1 ≤ ∏ i, f i
Full source
@[to_additive sum_nonneg]
lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod' fun _ _ ↦ hf _Informal description
Let $\iota$ be a finite type and let $f : \iota \to M$ be a function into an ordered commutative monoid $M$. If $1 \leq f(i)$ for all $i \in \iota$, then the product of $f$ over $\iota$ satisfies
\[ 1 \leq \prod_{i \in \iota} f(i). \]
Fintype.prod_le_one
theorem
(hf : f ≤ 1) : ∏ i, f i ≤ 1
Full source
@[to_additive] lemma prod_le_one (hf : f ≤ 1) : ∏ i, f i ≤ 1 := Finset.prod_le_one' fun _ _ ↦ hf _Informal description
Let $\iota$ be a finite type and let $f : \iota \to M$ be a function into an ordered commutative monoid $M$. If $f(i) \leq 1$ for all $i \in \iota$, then the product of $f$ over $\iota$ satisfies
\[ \prod_{i \in \iota} f(i) \leq 1. \]
Fintype.prod_eq_one_iff_of_one_le
theorem
(hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1
Full source
@[to_additive]
lemma prod_eq_one_iff_of_one_le (hf : 1 ≤ f) : ∏ i, f i∏ i, f i = 1 ↔ f = 1 :=
(Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans <| by simp [funext_iff]Informal description
Let $\iota$ be a finite type and let $f : \iota \to M$ be a function into an ordered commutative monoid $M$. If $1 \leq f(i)$ for all $i \in \iota$, then the product of $f$ over $\iota$ equals $1$ if and only if $f$ is the constant function equal to $1$. In other words,
\[ \prod_{i \in \iota} f(i) = 1 \leftrightarrow f = 1. \]
Fintype.prod_eq_one_iff_of_le_one
theorem
(hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1
Full source
@[to_additive]
lemma prod_eq_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i∏ i, f i = 1 ↔ f = 1 :=
(Finset.prod_eq_one_iff_of_le_one' fun i _ ↦ hf i).trans <| by simp [funext_iff]Informal description
Let $\iota$ be a finite type and let $f : \iota \to M$ be a function into an ordered commutative monoid $M$. If $f(i) \leq 1$ for all $i \in \iota$, then the product of $f$ over $\iota$ equals $1$ if and only if $f$ is the constant function equal to $1$. In other words,
\[ \prod_{i \in \iota} f(i) = 1 \leftrightarrow f = 1. \]
Fintype.prod_strictMono'
theorem
: StrictMono fun f : ι → M ↦ ∏ x, f x
Full source
@[to_additive sum_strictMono]
theorem prod_strictMono' : StrictMono fun f : ι → M ↦ ∏ x, f x :=
fun _ _ hfg ↦
let ⟨hle, i, hlt⟩ := Pi.lt_def.mp hfg
Finset.prod_lt_prod' (fun i _ ↦ hle i) ⟨i, Finset.mem_univ i, hlt⟩Informal description
Let $M$ be an ordered cancellative monoid and $\iota$ be a finite type. The function that maps a function $f \colon \iota \to M$ to the product $\prod_{x \in \iota} f(x)$ is strictly monotone. That is, if $f < g$ (pointwise), then $\prod_{x} f(x) < \prod_{x} g(x)$.
Fintype.one_lt_prod
theorem
(hf : 1 < f) : 1 < ∏ i, f i
Full source
@[to_additive sum_pos]
lemma one_lt_prod (hf : 1 < f) : 1 < ∏ i, f i :=
Finset.one_lt_prod' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2Informal description
Let $M$ be an ordered cancellative monoid and $\iota$ be a finite type. For any function $f \colon \iota \to M$ such that $1 < f(i)$ for all $i \in \iota$, the product $\prod_{i \in \iota} f(i)$ is strictly greater than $1$.
Fintype.prod_lt_one
theorem
(hf : f < 1) : ∏ i, f i < 1
Full source
@[to_additive]
lemma prod_lt_one (hf : f < 1) : ∏ i, f i < 1 :=
Finset.prod_lt_one' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2Informal description
Let $M$ be an ordered cancellative monoid and $\iota$ be a finite type. For any function $f \colon \iota \to M$ such that $f(i) < 1$ for all $i \in \iota$, the product $\prod_{i \in \iota} f(i)$ is strictly less than $1$.
Fintype.one_lt_prod_iff_of_one_le
theorem
(hf : 1 ≤ f) : 1 < ∏ i, f i ↔ 1 < f
Full source
@[to_additive sum_pos_iff_of_nonneg]
lemma one_lt_prod_iff_of_one_le (hf : 1 ≤ f) : 1 < ∏ i, f i ↔ 1 < f := by
obtain rfl | hf := hf.eq_or_lt <;> simp [*, one_lt_prod]Informal description
Let $f$ be a function from a finite type to an ordered cancellative monoid $\alpha$ such that $1 \leq f(i)$ for all $i$. Then the product $\prod_i f(i)$ is greater than $1$ if and only if there exists some $i$ such that $1 < f(i)$.
Fintype.prod_lt_one_iff_of_le_one
theorem
(hf : f ≤ 1) : ∏ i, f i < 1 ↔ f < 1
Full source
@[to_additive]
lemma prod_lt_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i∏ i, f i < 1 ↔ f < 1 := by
obtain rfl | hf := hf.eq_or_lt <;> simp [*, prod_lt_one]Informal description
Let $f$ be a function such that $f(i) \leq 1$ for all $i$. Then the product $\prod_i f(i)$ is less than $1$ if and only if there exists some $i$ such that $f(i) < 1$.
Multiset.finset_sum_eq_sup_iff_disjoint
theorem
[DecidableEq α] {i : Finset β} {f : β → Multiset α} :
i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
Full source
theorem finset_sum_eq_sup_iff_disjoint [DecidableEq α] {i : Finset β} {f : β → Multiset α} :
i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y) := by
induction' i using Finset.cons_induction_on with z i hz hr
· simp only [Finset.not_mem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
Finset.sup_empty, bot_eq_zero, eq_self_iff_true]
· simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
imp_and, forall_and, ← hr, @eq_comm _ z]
have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
simp +contextual only [this, not_false_iff, true_imp_iff]
simp_rw [← disjoint_finset_sum_left, ← disjoint_finset_sum_right, disjoint_comm, ← and_assoc,
and_self_iff]
exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))Informal description
For a finite set $i$ of type $\beta$ and a function $f \colon \beta \to \text{Multiset}(\alpha)$, the sum of $f$ over $i$ equals the supremum of $f$ over $i$ if and only if for any two distinct elements $x, y \in i$, the multisets $f(x)$ and $f(y)$ are disjoint. In symbols:
$$ \sum_{x \in i} f(x) = \sup_{x \in i} f(x) \leftrightarrow \forall x, y \in i, x \neq y \to f(x) \mathbin{\#} f(y). $$
Multiset.sup_powerset_len
theorem
[DecidableEq α] (x : Multiset α) : (Finset.sup (Finset.range (card x + 1)) fun k => x.powersetCard k) = x.powerset
Full source
theorem sup_powerset_len [DecidableEq α] (x : Multiset α) :
(Finset.sup (Finset.range (card x + 1)) fun k => x.powersetCard k) = x.powerset := by
convert bind_powerset_len x using 1
rw [Multiset.bind, Multiset.join, ← Finset.range_val, ← Finset.sum_eq_multiset_sum]
exact
Eq.symm (finset_sum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetCard x h)Informal description
For any multiset $x$ over a type $\alpha$ with decidable equality, the supremum of the family of multisets consisting of all subsets of $x$ with cardinality $k$, where $k$ ranges from $0$ to the cardinality of $x$, is equal to the powerset of $x$. In symbols:
$$ \sup_{k \in \{0, \dots, |x|\}} \{ y \subseteq x \mid |y| = k \} = \mathcal{P}(x). $$