FormContraction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Contraction of symmetric forms

The coefficients of a contraction are obtained by summing the original coefficients against the fixed vector. Evaluation is literally evaluation of that original form with the vector in the first slot. The proof reindexes all ordered basis tuples, including repeated indices and the empty remaining tuple.

def OAI.MetricEntropyDuality.SymmetricForm.contract line 30
Source documentation
Fix the first vector of a symmetric form, retaining its multiset coefficients.
```
def contract (v : Fin r → K) (F : SymmetricForm K r (j + 1)) :
    SymmetricForm K r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
theorem OAI.MetricEntropyDuality.SymmetricForm.contract_apply line 34
theorem OAI.MetricEntropyDuality.SymmetricForm.contract_zero line 38
theorem OAI.MetricEntropyDuality.SymmetricForm.contract_add line 43
theorem OAI.MetricEntropyDuality.SymmetricForm.contract_smul line 48
def OAI.MetricEntropyDuality.SymmetricForm.contractLinearMap line 60
Source documentation
The actual contraction map used as a partition label.
```
def contractLinearMap (v : Fin r → K) :
    SymmetricForm K r (j + 1) →ₗ[K] SymmetricForm K r j where
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
theorem OAI.MetricEntropyDuality.SymmetricForm.contractLinearMap_apply line 66
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_contract line 70
Source documentation
Coefficient contraction agrees with inserting the fixed vector into evaluation.
```
theorem eval_contract (v : Fin r → K) (F : SymmetricForm K r (j + 1))
    (args : Fin j → (Fin r → K)) :
    eval (contract v F) args = eval F (Fin.cons v args) := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.eval, OAI.MetricEntropyDuality.SymmetricForm.contract
theorem OAI.MetricEntropyDuality.SymmetricForm.contract_sub line 104