FormPolynomials.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomials of symmetric forms

The definitions sum over ordered basis tuples, exactly as the multilinear form evaluation does. The diagonal coefficient of a basis multiset is its ordered-tuple fiber cardinality times the value of the form. This coefficient is nonzero in characteristic greater than the degree. Renaming every vector block to the same coordinate proves nonvanishing for every index tuple, including tuples with repeated indices.

def OAI.MetricEntropyDuality.symExponent line 31
Source documentation
The exponent vector of a multiset of basis indices.
```
def symExponent {r h : ℕ} (s : Sym (Fin r) h) : Fin r →₀ ℕ :=
…
```
theorem OAI.MetricEntropyDuality.symExponent_injective line 34
theorem OAI.MetricEntropyDuality.symExponent_eq_iff line 40
theorem OAI.MetricEntropyDuality.symExponent_weight line 45
Source documentation
Every multiset exponent has precisely the prescribed total weight.
```
theorem symExponent_weight {r h : ℕ} (s : Sym (Fin r) h) :
    (symExponent s).sum (fun _ d => d) = h := by
…
```
Mentions: OAI.MetricEntropyDuality.symExponent
theorem OAI.MetricEntropyDuality.symExponent_tupleSym line 51
Source documentation
Passing from an ordered tuple to a monomial counts each occurrence.
```
theorem symExponent_tupleSym {r h : ℕ} (b : Fin h → Fin r) :
    symExponent (tupleSym b) = ∑ j : Fin h, Finsupp.single (b j) 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.symExponent, OAI.MetricEntropyDuality.tupleSym
def OAI.MetricEntropyDuality.diagonalPolynomial line 61
Source documentation
The diagonal polynomial, formed from the actual ordered-tuple expansion.
```
def diagonalPolynomial {K : Type uK} [CommSemiring K] {r h : ℕ}
    (F : SymmetricForm K r h) : MvPolynomial (Fin r) K :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
def OAI.MetricEntropyDuality.tuplePolynomial line 66
Source documentation
The actual symbolic evaluation on a tuple of vector blocks.
```
def tuplePolynomial {K : Type uK} [CommSemiring K] {r h u : ℕ}
    (F : SymmetricForm K r h) (a : Fin h → Fin u) :
    MvPolynomial (Fin u × Fin r) K :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
theorem OAI.MetricEntropyDuality.eval_diagonalPolynomial line 71
theorem OAI.MetricEntropyDuality.eval_tuplePolynomial line 77
theorem OAI.MetricEntropyDuality.rename_tuplePolynomial line 84
Source documentation
Identifying all blocks with one vector gives the diagonal polynomial.
```
theorem rename_tuplePolynomial {K : Type uK} [CommSemiring K] {r h u : ℕ}
    (F : SymmetricForm K r h) (a : Fin h → Fin u) :
    MvPolynomial.rename Prod.snd (tuplePolynomial F a) = diagonalPolynomial F := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tuplePolynomial, OAI.MetricEntropyDuality.diagonalPolynomial
theorem OAI.MetricEntropyDuality.totalDegree_tuplePolynomial_le line 89
theorem OAI.MetricEntropyDuality.totalDegree_diagonalPolynomial_le line 106
theorem OAI.MetricEntropyDuality.diagonal_term_eq_monomial line 117
theorem OAI.MetricEntropyDuality.coeff_diagonalPolynomial line 128
Source documentation
Distinct basis multisets yield distinct monomials. The coefficient is exactly the ordered-tuple multiplicity, including every repeated basis index.
```
theorem coeff_diagonalPolynomial {K : Type uK} [CommSemiring K] {r h : ℕ}
    (F : SymmetricForm K r h) (s : Sym (Fin r) h) :
    (diagonalPolynomial F).coeff (symExponent s) = (symFiberCard s : K) * F s := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.diagonalPolynomial, OAI.MetricEntropyDuality.symExponent, OAI.MetricEntropyDuality.symFiberCard
theorem OAI.MetricEntropyDuality.diagonalPolynomial_ne_zero line 146
Source documentation
Characteristic greater than the degree prevents diagonal cancellation.
```
theorem diagonalPolynomial_ne_zero {p r h : ℕ} [Fact p.Prime]
    (hp : h < p) (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0) :
    diagonalPolynomial F ≠ 0 := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.diagonalPolynomial
theorem OAI.MetricEntropyDuality.tuplePolynomial_ne_zero line 159
Source documentation
Every symbolic tuple evaluation is nonzero, with no distinct-index hypothesis. The proof includes all repeated-index patterns.
```
theorem tuplePolynomial_ne_zero {p r h u : ℕ} [Fact p.Prime]
    (hp : h < p) (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0)
    (a : Fin h → Fin u) : tuplePolynomial F a ≠ 0 := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tuplePolynomial
theorem OAI.MetricEntropyDuality.totalDegree_diagonalPolynomial line 167
Source documentation
The diagonal degree is exactly the form degree, including degree zero.
```
theorem totalDegree_diagonalPolynomial {p r h : ℕ} [Fact p.Prime]
    (hp : h < p) (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0) :
    (diagonalPolynomial F).totalDegree = h := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.diagonalPolynomial
theorem OAI.MetricEntropyDuality.totalDegree_tuplePolynomial line 181
Source documentation
Identifying vector blocks cannot increase degree, so every tuple has exactly degree h, even when its indices repeat.
```
theorem totalDegree_tuplePolynomial {p r h u : ℕ} [Fact p.Prime]
    (hp : h < p) (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0)
    (a : Fin h → Fin u) : (tuplePolynomial F a).totalDegree = h := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tuplePolynomial