SymmetricForms.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Literal coefficients and actual symmetric multilinear forms

A coefficient is assigned freely to every multiset of basis indices, including repetitions. Summing over ordered tuples gives an actual multilinear map. Basis evaluation recovers every coefficient, and every permutation-invariant multilinear map arises this way. The degree-zero case is included.

abbrev OAI.MetricEntropyDuality.SymmetricForm line 26
Source documentation
Free literal coefficients on multisets of basis indices.
```
abbrev SymmetricForm (K : Type uK) (r j : ℕ) := Sym (Fin r) j → K
…
```
def OAI.MetricEntropyDuality.SymmetricForm.eval line 33
Source documentation
Evaluation sums over ordered basis tuples; repeated indices are retained.
```
def eval (F : SymmetricForm K r j) (v : Fin j → (Fin r → K)) : K :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_zero line 36
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_add line 40
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_smul line 44
def OAI.MetricEntropyDuality.SymmetricForm.coordinateProduct line 48
theorem OAI.MetricEntropyDuality.SymmetricForm.coordinateProduct_apply line 53
def OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap line 57
Source documentation
The coefficient formula is an actual multilinear map, not an assumed law.
```
def toMultilinearMap (F : SymmetricForm K r j) :
    MultilinearMap K (fun _ : Fin j => Fin r → K) K :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_apply line 61
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_basis line 67
Source documentation
Evaluation at the specified basis tuple recovers its literal coefficient.
```
theorem eval_basis (F : SymmetricForm K r j) (a : Fin j → Fin r) :
    eval F (fun i => Pi.single (a i) (1 : K)) = F (tupleSym a) := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.eval, OAI.MetricEntropyDuality.tupleSym
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_injective line 84
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_domDomCongr line 95
Source documentation
Permuting the argument slots does not change the actual multilinear map.
```
theorem toMultilinearMap_domDomCongr (F : SymmetricForm K r j)
    (σ : Equiv.Perm (Fin j)) :
    (toMultilinearMap F).domDomCongr σ = toMultilinearMap F := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_comp_perm line 108
Source documentation
The evaluation is invariant under every permutation, including repeated vectors and the zero-degree tuple.
```
theorem eval_comp_perm (F : SymmetricForm K r j)
    (v : Fin j → (Fin r → K)) (σ : Equiv.Perm (Fin j)) :
    eval F (v ∘ σ) = eval F v := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.eval
def OAI.MetricEntropyDuality.SymmetricForm.IsSymmetric line 118
Source documentation
Symmetry as an actual property of a multilinear map.
```
def IsSymmetric (f : MultilinearMap K (fun _ : Fin j => Fin r → K) K) : Prop :=
…
```
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_isSymmetric line 121
def OAI.MetricEntropyDuality.SymmetricForm.representative line 126
theorem OAI.MetricEntropyDuality.SymmetricForm.tupleSym_representative line 129
def OAI.MetricEntropyDuality.SymmetricForm.ofMultilinearMap line 135
Source documentation
Read coefficients from actual basis evaluations. Symmetry will show that this does not depend on the representative selected for the multiset.
```
def ofMultilinearMap (f : MultilinearMap K (fun _ : Fin j => Fin r → K) K) :
    SymmetricForm K r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
theorem OAI.MetricEntropyDuality.SymmetricForm.ofMultilinearMap_tupleSym line 139
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_ofMultilinearMap line 155
Source documentation
Surjectivity onto the actual symmetric multilinear maps follows by basis extensionality; no characteristic restriction is required for this bridge.
```
theorem toMultilinearMap_ofMultilinearMap
    (f : MultilinearMap K (fun _ : Fin j => Fin r → K) K) (hf : IsSymmetric f) :
    toMultilinearMap (ofMultilinearMap f) = f := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm.IsSymmetric, OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap, OAI.MetricEntropyDuality.SymmetricForm.ofMultilinearMap
theorem OAI.MetricEntropyDuality.SymmetricForm.exists_toMultilinearMap line 163
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_add line 168
theorem OAI.MetricEntropyDuality.SymmetricForm.toMultilinearMap_smul line 173
def OAI.MetricEntropyDuality.SymmetricForm.invariantMultilinearSubmodule line 179
Source documentation
The symmetry condition is a linear subspace condition on actual maps.
```
def invariantMultilinearSubmodule (K : Type uK) [CommSemiring K] (r j : ℕ) :
    Submodule K (MultilinearMap K (fun _ : Fin j => Fin r → K) K) where
…
```
def OAI.MetricEntropyDuality.SymmetricForm.toInvariantMultilinear line 192
Source documentation
The concrete coefficient parametrization is linear into actual invariant multilinear maps.
```
def toInvariantMultilinear : SymmetricForm K r j →ₗ[K]
    invariantMultilinearSubmodule K r j where
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.invariantMultilinearSubmodule
def OAI.MetricEntropyDuality.SymmetricForm.equivInvariantMultilinear line 200
Source documentation
Free multiset coefficients and genuine symmetric multilinear maps describe exactly the same vector space.
```
def equivInvariantMultilinear : SymmetricForm K r j ≃ₗ[K]
    invariantMultilinearSubmodule K r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.invariantMultilinearSubmodule
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_neg line 211
theorem OAI.MetricEntropyDuality.SymmetricForm.eval_sub line 215