ImmDegree.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.matrix_list_prod_isHomogeneous line 13

Source documentation

A product of matrices whose entries are linear is homogeneous in its length.

theorem matrix_list_prod_isHomogeneous {σ ι : Type*} [Fintype ι] [DecidableEq ι]
    (L : List (Matrix ι ι (MvPolynomial σ K)))
    (hL : ∀ A ∈ L, ∀ i j, (A i j).IsHomogeneous 1) (i j : ι) :
    (L.prod i j).IsHomogeneous L.length := by
…

theorem OAI.Problem335.imm_isHomogeneous line 32
Source documentation
The iterated matrix multiplication polynomial has its expected degree.
```
theorem imm_isHomogeneous (K : Type*) [CommSemiring K] (n : ℕ) :
    (imm K n).IsHomogeneous n := by
…
```
Mentions: OAI.Problem335.imm

theorem OAI.Problem335.matrix_list_map_prod_isWeightedHomogeneous line 47

Source documentation

Matrix multiplication adds weighted degrees, including repeated layer occurrences.

theorem matrix_list_map_prod_isWeightedHomogeneous {σ ι τ M : Type*}
    [Fintype ι] [DecidableEq ι] [AddCommMonoid M]
    (w : σ → M) (A : τ → Matrix ι ι (MvPolynomial σ K)) (d : τ → M)
    (L : List τ) (hA : ∀ t ∈ L, ∀ i j, (A t i j).IsWeightedHomogeneous w (d t))
    (i j : ι) :
    ((L.map A).prod i j).IsWeightedHomogeneous w (L.map d).sum := by
…

theorem OAI.Problem335.imm_isWeightedHomogeneous line 67

Source documentation

Every monomial of IMM uses each matrix layer once, expressed with arbitrary additive weights.

theorem imm_isWeightedHomogeneous (K : Type*) [CommSemiring K] (n : ℕ)
    {M : Type*} [AddCommMonoid M] (w : Fin n → M) :
    (imm K n).IsWeightedHomogeneous (fun x => w x.1) (∑ t, w t) := by
…

Mentions: OAI.Problem335.imm

theorem OAI.Problem335.imm_layers_isWeightedHomogeneous line 81

Source documentation

The degree in any selected collection of matrix layers is its cardinality.

theorem imm_layers_isWeightedHomogeneous (K : Type*) [CommSemiring K] (n : ℕ)
    (s : Finset (Fin n)) :
    (imm K n).IsWeightedHomogeneous (fun x => if x.1 ∈ s then 1 else 0) s.card := by
…

Mentions: OAI.Problem335.imm

theorem OAI.Problem335.imm_support_layer_weight line 88

Source documentation

A support monomial has degree exactly one in each individual matrix layer.

theorem imm_support_layer_weight (K : Type*) [CommSemiring K] (n : ℕ)
    (t : Fin n) {d : (Fin n × Fin n × Fin n) →₀ ℕ} (hd : d ∈ (imm K n).support) :
    Finsupp.weight (fun x : Fin n × Fin n × Fin n => if x.1 = t then (1 : ℕ) else 0) d = 1 := by
…

Mentions: OAI.Problem335.imm

theorem OAI.Problem335.imm_degreeOf_le_one line 97
Source documentation
IMM is multilinear in every matrix-entry variable.
```
theorem imm_degreeOf_le_one (K : Type*) [CommSemiring K] (n : ℕ)
    (x : Fin n × Fin n × Fin n) : (imm K n).degreeOf x ≤ 1 := by
…
```
Mentions: OAI.Problem335.imm
def OAI.Problem335.immIdentityEvaluation line 114
Source documentation
Evaluation assigning every matrix layer the identity matrix.
```
def immIdentityEvaluation (K : Type*) [CommSemiring K] (n : ℕ) :
    MvPolynomial (Fin n × Fin n × Fin n) K →+* K :=
…
```
theorem OAI.Problem335.immIdentityEvaluation_layer line 118
theorem OAI.Problem335.immIdentityEvaluation_layers line 125
Source documentation
Evaluation at identity matrices sends any product of variable layers to the identity.
```
theorem immIdentityEvaluation_layers (n : ℕ) (L : List (Fin n)) :
    (immIdentityEvaluation K n).mapMatrix ((L.map (immLayer K n)).prod) = 1 := by
…
```
Mentions: OAI.Problem335.immIdentityEvaluation, OAI.Problem335.immLayer
theorem OAI.Problem335.immIdentityEvaluation_imm line 132
theorem OAI.Problem335.imm_ne_zero line 146
Source documentation
IMM does not vanish over any nontrivial coefficient semiring when its size is positive.
```
theorem imm_ne_zero (K : Type*) [CommSemiring K] [Nontrivial K] (n : ℕ) (hn : 0 < n) :
    imm K n ≠ 0 := by
…
```
Mentions: OAI.Problem335.imm
theorem OAI.Problem335.imm_totalDegree line 154
Source documentation
The total degree of IMM is the number of matrix layers.
```
theorem imm_totalDegree (K : Type*) [CommSemiring K] [Nontrivial K] (n : ℕ) :
    (imm K n).totalDegree = n := by
…
```
Mentions: OAI.Problem335.imm