Mathlib.Data.Multiset.Antidiagonal

Multiset.antidiagonal definition

(s : Multiset α) : Multiset (Multiset α × Multiset α)

Full source

/-- The antidiagonal of a multiset `s` consists of all pairs `(t₁, t₂)`
    such that `t₁ + t₂ = s`. These pairs are counted with multiplicities. -/
def antidiagonal (s : Multiset α) : Multiset (MultisetMultiset α × Multiset α) :=
  Quot.liftOn s (fun l ↦ (revzip (powersetAux l) : Multiset (MultisetMultiset α × Multiset α)))
    fun _ _ h ↦ Quot.sound (revzip_powersetAux_perm h)

Antidiagonal of a multiset

Informal description

For a multiset $s$ over a type $\alpha$, the antidiagonal of $s$ is the multiset of all pairs $(t_1, t_2)$ of multisets such that $t_1 + t_2 = s$, where addition is multiset addition. The pairs are counted with multiplicities corresponding to their occurrences in the construction.

Multiset.antidiagonal_coe theorem

(l : List α) : @antidiagonal α l = revzip (powersetAux l)

Full source

theorem antidiagonal_coe (l : List α) : @antidiagonal α l = revzip (powersetAux l) :=
  rfl

Antidiagonal of Multiset from List Equals Reverse Zip of Powerset

Informal description

For any list $l$ of elements of type $\alpha$, the antidiagonal of the multiset associated with $l$ is equal to the reverse zip of the auxiliary powerset of $l$. That is, if $s$ is the multiset corresponding to $l$, then the antidiagonal of $s$ consists of all pairs $(t_1, t_2)$ of multisets such that $t_1 + t_2 = s$, and this is constructed via the reverse zip operation applied to the auxiliary powerset of $l$.

Multiset.antidiagonal_coe' theorem

(l : List α) : @antidiagonal α l = revzip (powersetAux' l)

Full source

@[simp]
theorem antidiagonal_coe' (l : List α) : @antidiagonal α l = revzip (powersetAux' l) :=
  Quot.sound revzip_powersetAux_perm_aux'

Antidiagonal of List as Reverse Zip of Powerset

Informal description

For any list $l$ of elements of type $\alpha$, the antidiagonal of the multiset associated with $l$ is equal to the reverse zip of the auxiliary powerset of $l$.

Multiset.mem_antidiagonal theorem

{s : Multiset α} {x : Multiset α × Multiset α} : x ∈ antidiagonal s ↔ x.1 + x.2 = s

Full source

/-- A pair `(t₁, t₂)` of multisets is contained in `antidiagonal s`
    if and only if `t₁ + t₂ = s`. -/
@[simp]
theorem mem_antidiagonal {s : Multiset α} {x : MultisetMultiset α × Multiset α} :
    x ∈ antidiagonal sx ∈ antidiagonal s ↔ x.1 + x.2 = s :=
  Quotient.inductionOn s fun l ↦ by
    dsimp only [quot_mk_to_coe, antidiagonal_coe]
    refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩
    have _ := Classical.decEq α
    simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe,
      List.mem_map, mem_powersetAux]
    obtain ⟨x₁, x₂⟩ := x
    exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩

Characterization of Pairs in the Antidiagonal of a Multiset

Informal description

For a multiset $s$ over a type $\alpha$ and a pair of multisets $(t_1, t_2)$, the pair $(t_1, t_2)$ belongs to the antidiagonal of $s$ if and only if $t_1 + t_2 = s$, where $+$ denotes multiset addition.

Multiset.antidiagonal_map_fst theorem

(s : Multiset α) : (antidiagonal s).map Prod.fst = powerset s

Full source

@[simp]
theorem antidiagonal_map_fst (s : Multiset α) : (antidiagonal s).map Prod.fst = powerset s :=
  Quotient.inductionOn s fun l ↦ by simp [powersetAux']

First Projection of Antidiagonal Equals Powerset

Informal description

For any multiset $s$ over a type $\alpha$, the image of the antidiagonal of $s$ under the first projection map is equal to the powerset of $s$. In other words, if $\mathrm{antidiagonal}(s)$ is the multiset of all pairs $(t_1, t_2)$ such that $t_1 + t_2 = s$, then $\{t_1 \mid (t_1, t_2) \in \mathrm{antidiagonal}(s)\} = \mathrm{powerset}(s)$, where $\mathrm{powerset}(s)$ is the multiset of all submultisets of $s$.

Multiset.antidiagonal_map_snd theorem

(s : Multiset α) : (antidiagonal s).map Prod.snd = powerset s

Full source

@[simp]
theorem antidiagonal_map_snd (s : Multiset α) : (antidiagonal s).map Prod.snd = powerset s :=
  Quotient.inductionOn s fun l ↦ by simp [powersetAux']

Second Projection of Antidiagonal Equals Powerset

Informal description

For any multiset $s$ over a type $\alpha$, the image of the antidiagonal of $s$ under the second projection map $\mathrm{snd}$ is equal to the powerset of $s$. In other words, $\mathrm{snd} \circ \mathrm{antidiagonal}(s) = \mathrm{powerset}(s)$, where $\mathrm{powerset}(s)$ denotes the multiset of all submultisets of $s$.

Multiset.antidiagonal_zero theorem

: @antidiagonal α 0 = {(0, 0)}

Full source

@[simp]
theorem antidiagonal_zero : @antidiagonal α 0 = {(0, 0)} :=
  rfl

Antidiagonal of the Empty Multiset is $\{(0, 0)\}$

Informal description

The antidiagonal of the empty multiset is the singleton multiset containing the pair $(0, 0)$, where $0$ denotes the empty multiset.

Multiset.antidiagonal_cons theorem

 (a : α) (s) :
  antidiagonal (a ::ₘ s) = map (Prod.map id (cons a)) (antidiagonal s) + map (Prod.map (cons a) id) (antidiagonal s)

Full source

@[simp]
theorem antidiagonal_cons (a : α) (s) :
    antidiagonal (a ::ₘ s) =
      map (Prod.map id (cons a)) (antidiagonal s) + map (Prod.map (cons a) id) (antidiagonal s) :=
  Quotient.inductionOn s fun l ↦ by
    simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
      map_coe, antidiagonal_coe', coe_add]
    rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
    · congr
      · simp only [List.map_id]
      · rw [map_reverse]
      · simp
    · simp

Recursive Construction of Multiset Antidiagonal via Element Insertion

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the antidiagonal of the multiset obtained by inserting $a$ into $s$ (denoted $a ::ₘ s$) is equal to the sum of two multisets: 1. The image of the antidiagonal of $s$ under the map $(t_1, t_2) \mapsto (t_1, a ::ₘ t_2)$ 2. The image of the antidiagonal of $s$ under the map $(t_1, t_2) \mapsto (a ::ₘ t_1, t_2)$ In other words: $$\mathrm{antidiagonal}(a ::ₘ s) = \mathrm{map}\, (\lambda (t_1,t_2).\, (t_1, a ::ₘ t_2))\, (\mathrm{antidiagonal}\, s) + \mathrm{map}\, (\lambda (t_1,t_2).\, (a ::ₘ t_1, t_2))\, (\mathrm{antidiagonal}\, s)$$

Multiset.antidiagonal_eq_map_powerset theorem

[DecidableEq α] (s : Multiset α) : s.antidiagonal = s.powerset.map fun t ↦ (s - t, t)

Full source

theorem antidiagonal_eq_map_powerset [DecidableEq α] (s : Multiset α) :
    s.antidiagonal = s.powerset.map fun t ↦ (s - t, t) := by
  induction' s using Multiset.induction_on with a s hs
  · simp only [antidiagonal_zero, powerset_zero, Multiset.zero_sub, map_singleton]
  · simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
      id, sub_cons, erase_cons_head]
    rw [add_comm]
    congr 1
    refine Multiset.map_congr rfl fun x hx ↦ ?_
    rw [cons_sub_of_le _ (mem_powerset.mp hx)]

Antidiagonal as Image of Powerset under Complement Pairing

Informal description

For a multiset $s$ over a type $\alpha$ with decidable equality, the antidiagonal of $s$ is equal to the image of the powerset of $s$ under the map $t \mapsto (s - t, t)$, where $s - t$ denotes the multiset difference. In other words: $$\mathrm{antidiagonal}(s) = \mathrm{map}\, (\lambda t.\, (s - t, t))\, (\mathrm{powerset}\, s)$$

Multiset.card_antidiagonal theorem

(s : Multiset α) : card (antidiagonal s) = 2 ^ card s

Full source

@[simp]
theorem card_antidiagonal (s : Multiset α) : card (antidiagonal s) = 2 ^ card s := by
  have := card_powerset s
  rwa [← antidiagonal_map_fst, card_map] at this

Cardinality of Antidiagonal: $|\mathrm{antidiagonal}(s)| = 2^{|s|}$

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of the antidiagonal of $s$ is equal to $2$ raised to the power of the cardinality of $s$, i.e., $$|\mathrm{antidiagonal}(s)| = 2^{|s|}.$$