FormDimension.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Dimension of symmetric-form coefficients

The coefficients of a symmetric j-linear form on an r-dimensional space are indexed by multisets of j basis vectors. Their number gives the dimension of the coefficient space and hence its cardinality over a finite field.

def OAI.MetricEntropyDuality.formDimension line 21
Source documentation
The number of multisets of j basis vectors chosen from r vectors.
```
def formDimension (r j : ℕ) : ℕ := (r + j - 1).choose j
```
theorem OAI.MetricEntropyDuality.formDimension_pos line 24
Source documentation
Positive ambient dimension gives a nonempty coefficient index set.
```
theorem formDimension_pos {r j : ℕ} (hr : 0 < r) : 0 < formDimension r j := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.card_sym_fin line 28
Source documentation
Stars and bars counts the actual multiset coefficient indices.
```
theorem card_sym_fin (r j : ℕ) :
    Fintype.card (Sym (Fin r) j) = formDimension r j := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.card_form_coefficients line 34
Source documentation
A coefficient function over ZMod p has exactly p choices at each index.
```
theorem card_form_coefficients (p r j : ℕ) [NeZero p] :
    Fintype.card (Sym (Fin r) j → ZMod p) = p ^ formDimension r j := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.finrank_form_coefficients line 40
Source documentation
The coefficient space has one independent scalar coordinate per multiset.
```
theorem finrank_form_coefficients (K : Type uK) [Field K] (r j : ℕ) :
    Module.finrank K (Sym (Fin r) j → K) = formDimension r j := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension