SymmetricIndex.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Symmetric indices of tuples

A tuple is sent to its literal multiset of entries. Repeated entries are retained. Two tuples have the same index exactly when a permutation of their slots relates them.

def OAI.MetricEntropyDuality.tupleSym line 18
Source documentation
The multiset of entries of a tuple, including every repetition.
```
def tupleSym {r j : ℕ} (a : Fin j → Fin r) : Sym (Fin r) j :=
…
```
theorem OAI.MetricEntropyDuality.coe_tupleSym line 22
theorem OAI.MetricEntropyDuality.tupleSym_cons line 26
theorem OAI.MetricEntropyDuality.tupleSym_surjective line 32
Source documentation
Every multiset of the prescribed size is represented by a tuple.
```
theorem tupleSym_surjective (r j : ℕ) : Function.Surjective (@tupleSym r j) := by
…
```
Mentions: OAI.MetricEntropyDuality.tupleSym
theorem OAI.MetricEntropyDuality.tupleSym_comp_perm line 44
theorem OAI.MetricEntropyDuality.tupleSym_count line 50
Source documentation
A multiset count is the number of slots carrying that basis index.
```
theorem tupleSym_count {r j : ℕ} (a : Fin j → Fin r) (x : Fin r) :
    (tupleSym a : Multiset (Fin r)).count x = Fintype.card {i // a i = x} := by
…
```
Mentions: OAI.MetricEntropyDuality.tupleSym
theorem OAI.MetricEntropyDuality.tupleSym_eq_iff line 58
Source documentation
Equality of indices is precisely permutation of tuple slots.
```
theorem tupleSym_eq_iff {r j : ℕ} (a b : Fin j → Fin r) :
    tupleSym a = tupleSym b ↔ ∃ σ : Equiv.Perm (Fin j), a ∘ σ = b := by
…
```
Mentions: OAI.MetricEntropyDuality.tupleSym