PrescribedTuples.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Ordered tuples with a prescribed label multiset

A prescribed multiset may have repeated labels. Its ordered tuples embed in the permutations of one representative list, giving the uniform factorial bound. For a multiset without repetitions they are precisely the ordered tuples of its underlying finite set.

abbrev OAI.KadisonKastler.PrescribedLabelTuple line 25
instance OAI.KadisonKastler.(instance at line 28) line 28
def OAI.KadisonKastler.labelTupleSym line 33
def OAI.KadisonKastler.prescribedTupleSigmaEquiv line 38
Source documentation
Forgetting the prescribed multiset gives all label functions exactly once when the multiset itself is also summed over.
```
def prescribedTupleSigmaEquiv :
    (Σ s : Sym α r, PrescribedLabelTuple s) ≃ (Fin r → α) where
…
```
Mentions: OAI.KadisonKastler.PrescribedLabelTuple
theorem OAI.KadisonKastler.sum_labelTuples_by_multiset line 49
theorem OAI.KadisonKastler.card_prescribedLabelTuple_le line 60
Source documentation
Repetitions only reduce the number of distinct orderings.
```
theorem card_prescribedLabelTuple_le [Fintype α] (s : Sym α r) :
    Fintype.card (PrescribedLabelTuple s) ≤ r.factorial := by
…
```
Mentions: OAI.KadisonKastler.PrescribedLabelTuple
theorem OAI.KadisonKastler.prescribedLabelTuple_injective line 85
Source documentation
A prescribed tuple is injective exactly when its multiset has no repetitions.
```
theorem prescribedLabelTuple_injective (s : Sym α r) (hs : s.val.Nodup)
    (t : PrescribedLabelTuple s) : Function.Injective t.val := by
…
```
Mentions: OAI.KadisonKastler.PrescribedLabelTuple
theorem OAI.KadisonKastler.prescribedLabelTuple_mem line 92
def OAI.KadisonKastler.prescribedTupleOrderedEquiv line 100
Source documentation
In the distinct case, both tuple types have literally the same underlying label function.
```
def prescribedTupleOrderedEquiv (s : Sym α r) (hs : s.val.Nodup) :
    PrescribedLabelTuple s ≃ OrderedLabelTuple s.val.toFinset r where
…
```
Mentions: OAI.KadisonKastler.PrescribedLabelTuple, OAI.KadisonKastler.OrderedLabelTuple
theorem OAI.KadisonKastler.prescribedTupleOrderedEquiv_apply_val line 116
theorem OAI.KadisonKastler.prescribedTupleOrderedEquiv_symm_apply_val line 120

theorem OAI.KadisonKastler.sum_prescribedLabelTuple_eq_ordered line 125

Source documentation

Exact reindexing preserves every noncommutative word in the tuple.

theorem sum_prescribedLabelTuple_eq_ordered [Fintype α] {B : Type*} [AddCommMonoid B]
    (s : Sym α r) (hs : s.val.Nodup) (f : (Fin r → α) → B) :
    (∑ t : PrescribedLabelTuple s, f t.val) =
      ∑ t : OrderedLabelTuple s.val.toFinset r, f t.val := by
…

Mentions: OAI.KadisonKastler.PrescribedLabelTuple, OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.card_prescribedLabelTuple_of_nodup line 132