Mathlib.Data.Finsupp.Multiset

Finsupp.toMultiset definition

: (α →₀ ℕ) →+ Multiset α

Full source

/-- Given `f : α →₀ ℕ`, `f.toMultiset` is the multiset with multiplicities given by the values of
`f` on the elements of `α`. We define this function as an `AddMonoidHom`.

Under the additional assumption of `[DecidableEq α]`, this is available as
`Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ)`; the two declarations are separate as this assumption
is only needed for one direction. -/
def toMultiset : (α →₀ ℕ) →+ Multiset α where
  toFun f := Finsupp.sum f fun a n => n • {a}
  -- Porting note: have to specify `h` or add a `dsimp only` before `sum_add_index'`.
  -- see also: https://github.com/leanprover-community/mathlib4/issues/12129
  map_add' _f _g := sum_add_index' (h := fun _ n => n • _)
    (fun _ ↦ zero_nsmul _) (fun _ ↦ add_nsmul _)
  map_zero' := sum_zero_index

Multiset representation of finitely supported $\mathbb{N}$-valued functions

Informal description

Given a finitely supported function $f : \alpha \to_{\text{f}} \mathbb{N}$, the function `Finsupp.toMultiset` maps $f$ to the multiset over $\alpha$ where each element $a \in \alpha$ appears with multiplicity $f(a)$. This function is an additive monoid homomorphism, meaning it preserves the zero function and addition of functions.

Finsupp.toMultiset_zero theorem

: toMultiset (0 : α →₀ ℕ) = 0

Full source

theorem toMultiset_zero : toMultiset (0 : α →₀ ℕ) = 0 :=
  rfl

Multiset Representation of Zero Function is Empty Multiset

Informal description

The multiset representation of the zero function in finitely supported $\mathbb{N}$-valued functions is the empty multiset, i.e., $\text{toMultiset}(0) = 0$.

Finsupp.toMultiset_add theorem

(m n : α →₀ ℕ) : toMultiset (m + n) = toMultiset m + toMultiset n

Full source

theorem toMultiset_add (m n : α →₀ ℕ) : toMultiset (m + n) = toMultiset m + toMultiset n :=
  toMultiset.map_add m n

Additivity of Multiset Representation for Finitely Supported Functions

Informal description

For any two finitely supported $\mathbb{N}$-valued functions $m, n \colon \alpha \to_{\text{f}} \mathbb{N}$, the multiset representation of their sum $m + n$ is equal to the sum of their individual multiset representations, i.e., $\text{toMultiset}(m + n) = \text{toMultiset}(m) + \text{toMultiset}(n)$.

Finsupp.toMultiset_apply theorem

(f : α →₀ ℕ) : toMultiset f = f.sum fun a n => n • { a }

Full source

theorem toMultiset_apply (f : α →₀ ℕ) : toMultiset f = f.sum fun a n => n • {a} :=
  rfl

Multiset Representation of Finitely Supported $\mathbb{N}$-valued Functions

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$, the multiset representation `toMultiset f` is equal to the sum over all pairs $(a, n)$ in the support of $f$ of $n$ copies of the singleton multiset $\{a\}$. That is, \[ \text{toMultiset}(f) = \sum_{(a, n) \in f} n \cdot \{a\}. \]

Finsupp.toMultiset_single theorem

(a : α) (n : ℕ) : toMultiset (single a n) = n • { a }

Full source

@[simp]
theorem toMultiset_single (a : α) (n : ℕ) : toMultiset (single a n) = n • {a} := by
  rw [toMultiset_apply, sum_single_index]; apply zero_nsmul

Multiset Representation of Singleton Finitely Supported Function: $\text{toMultiset}(\text{single } a \, n) = n \cdot \{a\}$

Informal description

For any element $a$ of type $\alpha$ and any natural number $n$, the multiset representation of the finitely supported function `single a n` (which maps $a$ to $n$ and all other elements to zero) is equal to $n$ copies of the singleton multiset $\{a\}$, i.e., \[ \text{toMultiset}(\text{single } a \, n) = n \cdot \{a\}. \]

Finsupp.toMultiset_sum theorem

 {f : ι → α →₀ ℕ} (s : Finset ι) : Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i)

Full source

theorem toMultiset_sum {f : ι → α →₀ ℕ} (s : Finset ι) :
    Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i) :=
  map_sum Finsupp.toMultiset _ _

Multiset Sum Preservation under Finitely Supported Function Summation

Informal description

For any family of finitely supported $\mathbb{N}$-valued functions $f_i : \alpha \to_{\text{f}} \mathbb{N}$ indexed by $i \in \iota$ and any finite subset $s \subseteq \iota$, the multiset corresponding to the sum of the functions $\sum_{i \in s} f_i$ is equal to the sum of the multisets corresponding to each function $f_i$, i.e., \[ \text{toMultiset}\left(\sum_{i \in s} f_i\right) = \sum_{i \in s} \text{toMultiset}(f_i). \]

Finsupp.toMultiset_sum_single theorem

(s : Finset ι) (n : ℕ) : Finsupp.toMultiset (∑ i ∈ s, single i n) = n • s.val

Full source

theorem toMultiset_sum_single (s : Finset ι) (n : ℕ) :
    Finsupp.toMultiset (∑ i ∈ s, single i n) = n • s.val := by
  simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]

Multiset Sum of Singleton Functions Equals Scaled Base Set: $\text{toMultiset}(\sum_{i \in s} \text{single } i \, n) = n \cdot s$

Informal description

For any finite set $s$ of elements of type $\iota$ and any natural number $n$, the multiset obtained by applying `Finsupp.toMultiset` to the sum of `single i n` over all $i \in s$ is equal to $n$ times the underlying multiset of $s$, i.e., \[ \text{toMultiset}\left(\sum_{i \in s} \text{single } i \, n\right) = n \cdot s. \]

Finsupp.card_toMultiset theorem

(f : α →₀ ℕ) : Multiset.card (toMultiset f) = f.sum fun _ => id

Full source

@[simp]
theorem card_toMultiset (f : α →₀ ℕ) : Multiset.card (toMultiset f) = f.sum fun _ => id := by
  simp [toMultiset_apply, map_finsuppSum, Function.id_def]

Cardinality of Multiset Associated to Finitely Supported Function Equals Sum of Values

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$, the cardinality of the associated multiset $\text{toMultiset}(f)$ is equal to the sum of all values of $f$, i.e., \[ |\text{toMultiset}(f)| = \sum_{a \in \alpha} f(a). \]

Finsupp.toMultiset_map theorem

(f : α →₀ ℕ) (g : α → β) : f.toMultiset.map g = toMultiset (f.mapDomain g)

Full source

theorem toMultiset_map (f : α →₀ ℕ) (g : α → β) :
    f.toMultiset.map g = toMultiset (f.mapDomain g) := by
  refine f.induction ?_ ?_
  · rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
  · intro a n f _ _ ih
    rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single,
      toMultiset_single, toMultiset_add, toMultiset_single, ← Multiset.coe_mapAddMonoidHom,
      (Multiset.mapAddMonoidHom g).map_nsmul]
    rfl

Compatibility of Multiset Mapping with Domain Mapping for Finitely Supported Functions

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$ and any function $g \colon \alpha \to \beta$, the multiset obtained by applying $g$ to each element of the multiset representation of $f$ is equal to the multiset representation of the function obtained by mapping the domain of $f$ via $g$. That is, \[ \text{toMultiset}(f).\text{map}(g) = \text{toMultiset}(f.\text{mapDomain}(g)). \]

Finsupp.prod_toMultiset theorem

[CommMonoid α] (f : α →₀ ℕ) : f.toMultiset.prod = f.prod fun a n => a ^ n

Full source

@[to_additive (attr := simp)]
theorem prod_toMultiset [CommMonoid α] (f : α →₀ ℕ) :
    f.toMultiset.prod = f.prod fun a n => a ^ n := by
  refine f.induction ?_ ?_
  · rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
  · intro a n f _ _ ih
    rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
      Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
    exact pow_zero a

Product of Multiset Representation Equals Product of Function Values Raised to Their Powers

Informal description

Let $\alpha$ be a commutative monoid. For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$, the product of the elements in the multiset representation of $f$ is equal to the product over $\alpha$ of each element $a$ raised to the power of $f(a)$, i.e., \[ \prod (\text{toMultiset}(f)) = \prod_{a \in \alpha} a^{f(a)}. \]

Finsupp.toFinset_toMultiset theorem

[DecidableEq α] (f : α →₀ ℕ) : f.toMultiset.toFinset = f.support

Full source

@[simp]
theorem toFinset_toMultiset [DecidableEq α] (f : α →₀ ℕ) : f.toMultiset.toFinset = f.support := by
  refine f.induction ?_ ?_
  · rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
  · intro a n f ha hn ih
    rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
      support_single_ne_zero _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
    refine Disjoint.mono_left support_single_subset ?_
    rwa [Finset.disjoint_singleton_left]

Finset of Multiset Representation Equals Support of Finitely Supported Function

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$ with decidable equality on $\alpha$, the underlying finset of the multiset representation of $f$ is equal to the support of $f$, i.e., \[ \text{toFinset}(\text{toMultiset}(f)) = \text{supp}(f). \]

Finsupp.count_toMultiset theorem

[DecidableEq α] (f : α →₀ ℕ) (a : α) : (toMultiset f).count a = f a

Full source

@[simp]
theorem count_toMultiset [DecidableEq α] (f : α →₀ ℕ) (a : α) : (toMultiset f).count a = f a :=
  calc
    (toMultiset f).count a = Finsupp.sum f (fun x n => (n • {x} : Multiset α).count a) := by
      rw [toMultiset_apply]; exact map_sum (Multiset.countAddMonoidHom a) _ f.support
    _ = f.sum fun x n => n * ({x} : Multiset α).count a := by simp only [Multiset.count_nsmul]
    _ = f a * ({a} : Multiset α).count a :=
      sum_eq_single _
        (fun a' _ H => by simp only [Multiset.count_singleton, if_false, H.symm, mul_zero])
        (fun _ => zero_mul _)
    _ = f a := by rw [Multiset.count_singleton_self, mul_one]

Count in Multiset Representation Equals Function Value

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$ and any element $a \in \alpha$, the count of $a$ in the multiset representation of $f$ is equal to the value of $f$ at $a$, i.e., \[ \text{count}_a(\text{toMultiset}(f)) = f(a). \]

Finsupp.toMultiset_sup theorem

[DecidableEq α] (f g : α →₀ ℕ) : toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g

Full source

theorem toMultiset_sup [DecidableEq α] (f g : α →₀ ℕ) :
    toMultiset (f ⊔ g) = toMultisettoMultiset f ∪ toMultiset g := by
  ext
  simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]

Multiset Representation Preserves Pointwise Supremum of Finitely Supported Functions

Informal description

For any finitely supported $\mathbb{N}$-valued functions $f, g \colon \alpha \to_{\text{f}} \mathbb{N}$, the multiset representation of the pointwise supremum $f \sqcup g$ is equal to the union of the multiset representations of $f$ and $g$, i.e., \[ \text{toMultiset}(f \sqcup g) = \text{toMultiset}(f) \cup \text{toMultiset}(g). \]

Finsupp.toMultiset_inf theorem

[DecidableEq α] (f g : α →₀ ℕ) : toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g

Full source

theorem toMultiset_inf [DecidableEq α] (f g : α →₀ ℕ) :
    toMultiset (f ⊓ g) = toMultisettoMultiset f ∩ toMultiset g := by
  ext
  simp_rw [Multiset.count_inter, Finsupp.count_toMultiset, Finsupp.inf_apply]

Multiset Representation Preserves Pointwise Infimum of Finitely Supported Functions

Informal description

For any two finitely supported functions $f, g \colon \alpha \to_{\text{f}} \mathbb{N}$, the multiset representation of the pointwise infimum $f \sqcap g$ is equal to the intersection of the multiset representations of $f$ and $g$. That is, \[ \text{toMultiset}(f \sqcap g) = \text{toMultiset}(f) \cap \text{toMultiset}(g). \]

Finsupp.mem_toMultiset theorem

(f : α →₀ ℕ) (i : α) : i ∈ toMultiset f ↔ i ∈ f.support

Full source

@[simp]
theorem mem_toMultiset (f : α →₀ ℕ) (i : α) : i ∈ toMultiset fi ∈ toMultiset f ↔ i ∈ f.support := by
  classical
  rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]

Membership in Multiset Representation of Finitely Supported Function Corresponds to Support Membership

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$ and any element $i \in \alpha$, the element $i$ belongs to the multiset representation of $f$ if and only if $i$ is in the support of $f$, i.e., $i \in \text{toMultiset}(f) \leftrightarrow i \in \text{support}(f)$.

Multiset.toFinsupp definition

: Multiset α ≃+ (α →₀ ℕ)

Full source

/-- Given a multiset `s`, `s.toFinsupp` returns the finitely supported function on `ℕ` given by
the multiplicities of the elements of `s`. -/
@[simps symm_apply]
def toFinsupp : MultisetMultiset α ≃+ (α →₀ ℕ) where
  toFun s := ⟨s.toFinset, fun a => s.count a, fun a => by simp⟩
  invFun f := Finsupp.toMultiset f
  map_add' _ _ := Finsupp.ext fun _ => count_add _ _ _
  right_inv f :=
    Finsupp.ext fun a => by
      simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum',
        Multiset.count_singleton, mul_boole, Finsupp.coe_mk, Finsupp.mem_support_iff,
        Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
      exact Eq.symm
  left_inv s := by simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk,
    Multiset.toFinset_sum_count_nsmul_eq]

Multiset to finitely supported function equivalence

Informal description

Given a multiset $s$ over a type $\alpha$, the function $\text{toFinsupp}$ maps $s$ to a finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$, where $f(a)$ is the multiplicity of $a$ in $s$ for each $a \in \alpha$. This function forms an additive equivalence between multisets over $\alpha$ and finitely supported $\mathbb{N}$-valued functions on $\alpha$, meaning it preserves the additive structure (zero and addition) and is bijective.

Multiset.toFinsupp_support theorem

(s : Multiset α) : s.toFinsupp.support = s.toFinset

Full source

@[simp]
theorem toFinsupp_support (s : Multiset α) : s.toFinsupp.support = s.toFinset := rfl

Support of Multiset-to-Finsupp Equals Underlying Finset

Informal description

For any multiset $s$ over a type $\alpha$, the support of the finitely supported function $\text{toFinsupp}(s)$ is equal to the underlying finset of $s$, i.e., $\text{support}(\text{toFinsupp}(s)) = \text{toFinset}(s)$.

Multiset.toFinsupp_apply theorem

(s : Multiset α) (a : α) : toFinsupp s a = s.count a

Full source

@[simp]
theorem toFinsupp_apply (s : Multiset α) (a : α) : toFinsupp s a = s.count a := rfl

Multiset-to-Finsupp Function Counts Elements

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, the value of the finitely supported function $\text{toFinsupp}(s)$ at $a$ is equal to the count of $a$ in $s$, i.e., $\text{toFinsupp}(s)(a) = \text{count}(a, s)$.

Multiset.toFinsupp_zero theorem

: toFinsupp (0 : Multiset α) = 0

Full source

theorem toFinsupp_zero : toFinsupp (0 : Multiset α) = 0 := _root_.map_zero _

Empty Multiset Maps to Zero Function under `toFinsupp`

Informal description

The finitely supported function corresponding to the empty multiset is the zero function, i.e., $\text{toFinsupp}(0) = 0$.

Multiset.toFinsupp_add theorem

(s t : Multiset α) : toFinsupp (s + t) = toFinsupp s + toFinsupp t

Full source

theorem toFinsupp_add (s t : Multiset α) : toFinsupp (s + t) = toFinsupp s + toFinsupp t :=
  _root_.map_add toFinsupp s t

Additivity of Multiset to Finitely Supported Function Conversion

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the finitely supported function corresponding to their sum $s + t$ is equal to the sum of the finitely supported functions corresponding to $s$ and $t$ individually. That is, $\text{toFinsupp}(s + t) = \text{toFinsupp}(s) + \text{toFinsupp}(t)$.

Multiset.toFinsupp_singleton theorem

(a : α) : toFinsupp ({ a } : Multiset α) = Finsupp.single a 1

Full source

@[simp]
theorem toFinsupp_singleton (a : α) : toFinsupp ({a} : Multiset α) = Finsupp.single a 1 := by
  ext; rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]

Singleton Multiset Maps to Indicator Function under `toFinsupp`

Informal description

For any element $a$ of type $\alpha$, the finitely supported function corresponding to the singleton multiset $\{a\}$ is equal to the function that maps $a$ to $1$ and all other elements to $0$, i.e., $\text{toFinsupp}(\{a\}) = \text{single}_a(1)$.

Multiset.toFinsupp_toMultiset theorem

(s : Multiset α) : Finsupp.toMultiset (toFinsupp s) = s

Full source

@[simp]
theorem toFinsupp_toMultiset (s : Multiset α) : Finsupp.toMultiset (toFinsupp s) = s :=
  Multiset.toFinsupp.symm_apply_apply s

Multiset-Finsupp Equivalence: Roundtrip from Multiset to Finsupp and Back

Informal description

For any multiset $s$ over a type $\alpha$, the composition of the functions `toFinsupp` and `Finsupp.toMultiset` maps $s$ back to itself, i.e., $\text{Finsupp.toMultiset}(\text{toFinsupp}(s)) = s$.

Multiset.toFinsupp_eq_iff theorem

{s : Multiset α} {f : α →₀ ℕ} : toFinsupp s = f ↔ s = Finsupp.toMultiset f

Full source

theorem toFinsupp_eq_iff {s : Multiset α} {f : α →₀ ℕ} :
    toFinsupptoFinsupp s = f ↔ s = Finsupp.toMultiset f :=
  Multiset.toFinsupp.apply_eq_iff_symm_apply

Equivalence between Multisets and Finitely Supported $\mathbb{N}$-valued Functions

Informal description

For any multiset $s$ over a type $\alpha$ and any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$, the equivalence $\text{toFinsupp}(s) = f$ holds if and only if $s$ is equal to the multiset representation of $f$, i.e., $s = \text{Finsupp.toMultiset}(f)$.

Multiset.toFinsupp_union theorem

(s t : Multiset α) : toFinsupp (s ∪ t) = toFinsupp s ⊔ toFinsupp t

Full source

theorem toFinsupp_union (s t : Multiset α) : toFinsupp (s ∪ t) = toFinsupptoFinsupp s ⊔ toFinsupp t := by
  ext
  simp

Union of Multisets Corresponds to Supremum of Finitely Supported Functions

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the finitely supported function corresponding to their union $s \cup t$ is equal to the pointwise supremum of the finitely supported functions corresponding to $s$ and $t$, i.e., $$\text{toFinsupp}(s \cup t) = \text{toFinsupp}(s) \sqcup \text{toFinsupp}(t).$$

Multiset.toFinsupp_inter theorem

(s t : Multiset α) : toFinsupp (s ∩ t) = toFinsupp s ⊓ toFinsupp t

Full source

theorem toFinsupp_inter (s t : Multiset α) : toFinsupp (s ∩ t) = toFinsupptoFinsupp s ⊓ toFinsupp t := by
  ext
  simp

Intersection of Multisets Corresponds to Infimum of Finitely Supported Functions

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the finitely supported $\mathbb{N}$-valued function corresponding to their intersection $s \cap t$ is equal to the infimum (meet) of the finitely supported functions corresponding to $s$ and $t$. That is, $\text{toFinsupp}(s \cap t) = \text{toFinsupp}(s) \sqcap \text{toFinsupp}(t)$.

Multiset.toFinsupp_sum_eq theorem

(s : Multiset α) : s.toFinsupp.sum (fun _ ↦ id) = Multiset.card s

Full source

@[simp]
theorem toFinsupp_sum_eq (s : Multiset α) : s.toFinsupp.sum (fun _ ↦ id) = Multiset.card s := by
  rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]

Sum of Finsupp Values Equals Multiset Cardinality

Informal description

For any multiset $s$ over a type $\alpha$, the sum of the values of the corresponding finitely supported function $s.\text{toFinsupp}$ is equal to the cardinality of $s$, i.e., \[ \sum_{a \in \alpha} (s.\text{toFinsupp})(a) = |s|. \]

Finsupp.toMultiset_toFinsupp theorem

[DecidableEq α] (f : α →₀ ℕ) : Multiset.toFinsupp (Finsupp.toMultiset f) = f

Full source

@[simp]
theorem Finsupp.toMultiset_toFinsupp [DecidableEq α] (f : α →₀ ℕ) :
    Multiset.toFinsupp (Finsupp.toMultiset f) = f :=
  Multiset.toFinsupp.apply_symm_apply _

Recovery of Finitely Supported Function via Multiset Conversion

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$, the composition of the functions `Finsupp.toMultiset` and `Multiset.toFinsupp` recovers the original function, i.e., $\text{toFinsupp}(\text{toMultiset}(f)) = f$.

Finsupp.toMultiset_eq_iff theorem

[DecidableEq α] {f : α →₀ ℕ} {s : Multiset α} : Finsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s

Full source

theorem Finsupp.toMultiset_eq_iff [DecidableEq α] {f : α →₀ ℕ} {s : Multiset α} :
    Finsupp.toMultisetFinsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s :=
  Multiset.toFinsupp.symm_apply_eq

Equivalence between Multiset and Finitely Supported Function Representations

Informal description

For a finitely supported function $f \colon \alpha \to_{\text{f}} \mathbb{N}$ and a multiset $s$ over $\alpha$, the multiset representation of $f$ equals $s$ if and only if $f$ equals the finitely supported function representation of $s$. In other words, $Finsupp.toMultiset(f) = s \leftrightarrow f = Multiset.toFinsupp(s)$.

Finsupp.orderIsoMultiset definition

[DecidableEq ι] : (ι →₀ ℕ) ≃o Multiset ι

Full source

/-- `Finsupp.toMultiset` as an order isomorphism. -/
def orderIsoMultiset [DecidableEq ι] : (ι →₀ ℕ) ≃o Multiset ι where
  toEquiv := Multiset.toFinsupp.symm.toEquiv
  map_rel_iff' {f g} := by simp [le_def, Multiset.le_iff_count]

Order isomorphism between finitely supported functions and multisets

Informal description

The order isomorphism `Finsupp.orderIsoMultiset` establishes an equivalence between finitely supported functions `ι →₀ ℕ` and multisets over `ι`, where the order on both sides is preserved. Specifically, for any two finitely supported functions `f` and `g`, `f ≤ g` if and only if the corresponding multisets satisfy the same inequality pointwise.

Finsupp.coe_orderIsoMultiset theorem

[DecidableEq ι] : ⇑(@orderIsoMultiset ι _) = toMultiset

Full source

@[simp]
theorem coe_orderIsoMultiset [DecidableEq ι] : ⇑(@orderIsoMultiset ι _) = toMultiset :=
  rfl

Underlying Function of Order Isomorphism Equals `Finsupp.toMultiset`

Informal description

For any type $\iota$ with decidable equality, the underlying function of the order isomorphism `Finsupp.orderIsoMultiset` is equal to the function `Finsupp.toMultiset`, which maps finitely supported $\mathbb{N}$-valued functions to multisets over $\iota$.

Finsupp.coe_orderIsoMultiset_symm theorem

[DecidableEq ι] : ⇑(@orderIsoMultiset ι).symm = Multiset.toFinsupp

Full source

@[simp]
theorem coe_orderIsoMultiset_symm [DecidableEq ι] :
    ⇑(@orderIsoMultiset ι).symm = Multiset.toFinsupp :=
  rfl

Inverse of Order Isomorphism Between Finitely Supported Functions and Multisets is `Multiset.toFinsupp`

Informal description

For any type $\iota$ with decidable equality, the underlying function of the inverse of the order isomorphism `orderIsoMultiset` is equal to the function `Multiset.toFinsupp`, which maps a multiset over $\iota$ to a finitely supported $\mathbb{N}$-valued function on $\iota$.

Finsupp.toMultiset_strictMono theorem

: StrictMono (@toMultiset ι)

Full source

theorem toMultiset_strictMono : StrictMono (@toMultiset ι) := by
  classical exact (@orderIsoMultiset ι _).strictMono

Strict Monotonicity of the Multiset Representation of Finitely Supported Functions

Informal description

The function `Finsupp.toMultiset`, which maps finitely supported $\mathbb{N}$-valued functions on $\iota$ to multisets over $\iota$, is strictly monotone. That is, for any two functions $m, n : \iota \to_{\text{f}} \mathbb{N}$, if $m < n$ in the pointwise order, then the corresponding multisets satisfy $\text{toMultiset}(m) < \text{toMultiset}(n)$.

Finsupp.sum_id_lt_of_lt theorem

(m n : ι →₀ ℕ) (h : m < n) : (m.sum fun _ => id) < n.sum fun _ => id

Full source

theorem sum_id_lt_of_lt (m n : ι →₀ ℕ) (h : m < n) : (m.sum fun _ => id) < n.sum fun _ => id := by
  rw [← card_toMultiset, ← card_toMultiset]
  apply Multiset.card_lt_card
  exact toMultiset_strictMono h

Sum of Values Increases with Pointwise Order on Finitely Supported $\mathbb{N}$-valued Functions

Informal description

For any two finitely supported $\mathbb{N}$-valued functions $m, n \colon \iota \to_{\text{f}} \mathbb{N}$ such that $m < n$ in the pointwise order, the sum of the values of $m$ is strictly less than the sum of the values of $n$, i.e., \[ \sum_{a \in \iota} m(a) < \sum_{a \in \iota} n(a). \]

Finsupp.lt_wf theorem

: WellFounded (@LT.lt (ι →₀ ℕ) _)

Full source

/-- The order on `ι →₀ ℕ` is well-founded. -/
theorem lt_wf : WellFounded (@LT.lt (ι →₀ ℕ) _) :=
  Subrelation.wf (sum_id_lt_of_lt _ _) <| InvImage.wf _ Nat.lt_wfRel.2

Well-foundedness of the pointwise order on finitely supported $\mathbb{N}$-valued functions

Informal description

The strict less-than relation `<` on the type of finitely supported $\mathbb{N}$-valued functions $\iota \to_{\text{f}} \mathbb{N}$ is well-founded. That is, there are no infinite descending chains with respect to this order.

Finsupp.instWellFoundedRelationNat instance

: WellFoundedRelation (ι →₀ ℕ)

Full source

instance : WellFoundedRelation (ι →₀ ℕ) where
  rel := (· < ·)
  wf := lt_wf _

Well-founded Order on Finitely Supported $\mathbb{N}$-valued Functions

Informal description

The type of finitely supported $\mathbb{N}$-valued functions $\iota \to_{\text{f}} \mathbb{N}$ is equipped with a well-founded relation, where the strict less-than relation `<` is well-founded. This means there are no infinite descending chains with respect to this order.

Multiset.toFinsupp_strictMono theorem

[DecidableEq ι] : StrictMono (@Multiset.toFinsupp ι _)

Full source

theorem Multiset.toFinsupp_strictMono [DecidableEq ι] : StrictMono (@Multiset.toFinsupp ι _) :=
  (@Finsupp.orderIsoMultiset ι).symm.strictMono

Strict Monotonicity of Multiset-to-Finsupp Conversion

Informal description

For any type $\iota$ with decidable equality, the function $\text{toFinsupp} \colon \text{Multiset} \ \iota \to (\iota \to_{\text{f}} \mathbb{N})$ is strictly monotone. That is, for any two multisets $s_1$ and $s_2$ over $\iota$, if $s_1 < s_2$ in the multiset order, then $\text{toFinsupp}(s_1) < \text{toFinsupp}(s_2)$ in the pointwise order on finitely supported functions.

Sym.equivNatSum definition

: Sym α n ≃ { P : α →₀ ℕ // P.sum (fun _ ↦ id) = n }

Full source

/-- The `n`th symmetric power of a type `α` is naturally equivalent to the subtype of
finitely-supported maps `α →₀ ℕ` with total mass `n`.

See also `Sym.equivNatSumOfFintype` when `α` is finite. -/
def equivNatSum :
    SymSym α n ≃ {P : α →₀ ℕ // P.sum (fun _ ↦ id) = n} :=
  Multiset.toFinsupp.toEquiv.subtypeEquiv <| by simp

Equivalence between symmetric power and finitely supported functions with fixed sum

Informal description

The $n$th symmetric power of a type $\alpha$ is naturally in bijection with the set of finitely supported functions $P \colon \alpha \to \mathbb{N}$ such that the sum of $P$ over all elements of $\alpha$ equals $n$. More precisely, the equivalence maps a multiset $s$ in $\text{Sym}(\alpha, n)$ to the function counting the multiplicity of each element in $s$, and conversely, it maps a finitely supported function $P$ with total sum $n$ to the multiset where each element $a \in \alpha$ appears $P(a)$ times.

Sym.coe_equivNatSum_apply_apply theorem

(s : Sym α n) (a : α) : (equivNatSum α n s : α →₀ ℕ) a = (s : Multiset α).count a

Full source

@[simp] lemma coe_equivNatSum_apply_apply (s : Sym α n) (a : α) :
    (equivNatSum α n s : α →₀ ℕ) a = (s : Multiset α).count a :=
  rfl

Multiplicity-Count Equivalence in Symmetric Power

Informal description

For any symmetric power element $s \in \text{Sym}(\alpha, n)$ and any element $a \in \alpha$, the multiplicity of $a$ in the finitely supported function corresponding to $s$ via the equivalence $\text{equivNatSum}$ is equal to the count of $a$ in the multiset representation of $s$. In symbols: $(\text{equivNatSum}_{\alpha,n}(s))(a) = \text{count}(a, s)$.

Sym.coe_equivNatSum_symm_apply theorem

 (P : { P : α →₀ ℕ // P.sum (fun _ ↦ id) = n }) : ((equivNatSum α n).symm P : Multiset α) = Finsupp.toMultiset P

Full source

@[simp] lemma coe_equivNatSum_symm_apply (P : {P : α →₀ ℕ // P.sum (fun _ ↦ id) = n}) :
    ((equivNatSum α n).symm P : Multiset α) = Finsupp.toMultiset P :=
  rfl

Multiset Representation of Finitely Supported Functions via Inverse Equivalence

Informal description

For any finitely supported function $P \colon \alpha \to \mathbb{N}$ with total sum $\sum_{a \in \alpha} P(a) = n$, the multiset obtained by applying the inverse of the equivalence `equivNatSum` to $P$ is equal to the multiset representation of $P$ via `Finsupp.toMultiset`. More precisely, if $P$ is a finitely supported $\mathbb{N}$-valued function on $\alpha$ with total sum $n$, then the multiset corresponding to $P$ under the inverse of `equivNatSum` is the multiset where each element $a \in \alpha$ appears with multiplicity $P(a)$.

Sym.equivNatSumOfFintype definition

[Fintype α] : Sym α n ≃ { P : α → ℕ // ∑ i, P i = n }

Full source

/-- The `n`th symmetric power of a finite type `α` is naturally equivalent to the subtype of maps
`α → ℕ` with total mass `n`.

See also `Sym.equivNatSum` when `α` is not necessarily finite. -/
noncomputable def equivNatSumOfFintype [Fintype α] :
    SymSym α n ≃ {P : α → ℕ // ∑ i, P i = n} :=
  (equivNatSum α n).trans <| Finsupp.equivFunOnFinite.subtypeEquiv <| by simp [Finsupp.sum_fintype]

Equivalence between symmetric power and functions with fixed sum on a finite type

Informal description

For a finite type $\alpha$ and a natural number $n$, the $n$th symmetric power of $\alpha$ is equivalent to the set of functions $P \colon \alpha \to \mathbb{N}$ such that the sum of $P$ over all elements of $\alpha$ equals $n$. More precisely, the equivalence maps a multiset $s$ in $\text{Sym}(\alpha, n)$ to the function that counts the multiplicity of each element in $s$, and conversely, it maps a function $P$ with total sum $n$ to the multiset where each element $a \in \alpha$ appears $P(a)$ times.

Sym.coe_equivNatSumOfFintype_apply_apply theorem

[Fintype α] (s : Sym α n) (a : α) : (equivNatSumOfFintype α n s : α → ℕ) a = (s : Multiset α).count a

Full source

@[simp] lemma coe_equivNatSumOfFintype_apply_apply [Fintype α] (s : Sym α n) (a : α) :
    (equivNatSumOfFintype α n s : α → ℕ) a = (s : Multiset α).count a :=
  rfl

Multiplicity-Count Correspondence in Symmetric Power Equivalence

Informal description

For a finite type $\alpha$ and a natural number $n$, given a multiset $s$ in the $n$th symmetric power of $\alpha$ and an element $a \in \alpha$, the multiplicity of $a$ in the function representation of $s$ (via `equivNatSumOfFintype`) equals the count of $a$ in the multiset $s$. In other words, if $P = \text{equivNatSumOfFintype}(s)$ is the $\mathbb{N}$-valued function corresponding to $s$, then $P(a) = \text{count}(s, a)$ for any $a \in \alpha$.

Sym.coe_equivNatSumOfFintype_symm_apply theorem

 [Fintype α] (P : { P : α → ℕ // ∑ i, P i = n }) :
  ((equivNatSumOfFintype α n).symm P : Multiset α) = ∑ a, ((P : α → ℕ) a) • { a }

Full source

@[simp] lemma coe_equivNatSumOfFintype_symm_apply [Fintype α] (P : {P : α → ℕ // ∑ i, P i = n}) :
    ((equivNatSumOfFintype α n).symm P : Multiset α) = ∑ a, ((P : α → ℕ) a) • {a} := by
  obtain ⟨P, hP⟩ := P
  change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _
  ext a
  rw [Multiset.count_sum]
  simp [Multiset.count_singleton]

Multiset Representation of Fixed-Sum Functions via Inverse Equivalence

Informal description

For a finite type $\alpha$ and a natural number $n$, let $P \colon \alpha \to \mathbb{N}$ be a function such that $\sum_{a \in \alpha} P(a) = n$. Then, the multiset corresponding to $P$ under the inverse of the equivalence `equivNatSumOfFintype` is given by the formal sum $\sum_{a \in \alpha} P(a) \cdot \{a\}$, where $\{a\}$ denotes the singleton multiset containing $a$. In other words, the multiset obtained by applying the inverse of `equivNatSumOfFintype` to $P$ is the multiset where each element $a \in \alpha$ appears with multiplicity $P(a)$.