SymmetricMultiplicity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Multiplicities of symmetric indices

The tuples representing a fixed multiset form a permutation orbit. Its size is positive and divides the factorial of the number of slots. Consequently the coefficient multiplicity cannot vanish modulo a prime larger than that number.

def OAI.MetricEntropyDuality.symFiberCard line 20
Source documentation
Number of ordered tuples representing the given multiset.
```
def symFiberCard {r j : ℕ} (s : Sym (Fin r) j) : ℕ :=
…
```
theorem OAI.MetricEntropyDuality.symFiberCard_pos line 24
Source documentation
Every symmetric index has at least one ordered representative.
```
theorem symFiberCard_pos {r j : ℕ} (s : Sym (Fin r) j) : 0 < symFiberCard s := by
…
```
Mentions: OAI.MetricEntropyDuality.symFiberCard
theorem OAI.MetricEntropyDuality.symFiberCard_dvd_factorial line 29
Source documentation
The actual tuple fiber is a permutation orbit, so its size divides j!.
```
theorem symFiberCard_dvd_factorial {r j : ℕ} (s : Sym (Fin r) j) :
    symFiberCard s ∣ j.factorial := by
…
```
Mentions: OAI.MetricEntropyDuality.symFiberCard
theorem OAI.MetricEntropyDuality.not_dvd_symFiberCard line 53
Source documentation
No prime larger than the tuple length divides its multiplicity.
```
theorem not_dvd_symFiberCard {r j p : ℕ} (s : Sym (Fin r) j)
    (hp : p.Prime) (hjp : j < p) : ¬ p ∣ symFiberCard s := by
…
```
Mentions: OAI.MetricEntropyDuality.symFiberCard
theorem OAI.MetricEntropyDuality.symFiberCard_cast_ne_zero line 59
Source documentation
The diagonal coefficient multiplicity is nonzero in the required field.
```
theorem symFiberCard_cast_ne_zero {r j p : ℕ} (s : Sym (Fin r) j)
    (hp : p.Prime) (hjp : j < p) : (symFiberCard s : ZMod p) ≠ 0 := by
…
```
Mentions: OAI.MetricEntropyDuality.symFiberCard