AmbientCoefficient.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PermanentBorder.AmbientPolar.groupIndex line 10
Source documentation
H,U,V are respectively none, some false, some true.
```
def groupIndex : Option Bool → Fin 3
  | none => 0
  | some false => 1
  | some true => 2
```
lemma OAI.PermanentBorder.AmbientPolar.groupIndex_injective line 15
lemma OAI.PermanentBorder.AmbientPolar.dimensions_explicit line 18

lemma OAI.PermanentBorder.AmbientPolar.literal_coefficient_eq line 30

Source documentation

The three-variable coefficient equals the mixed coefficient for matrices of size n + 1.

lemma literal_coefficient_eq (K n : ℕ) :
    ((X (0 : Fin 3) + X 1)^(n+1) * (X 0 + X 2)^n *
      (X 1 + X 2)^K : MvPolynomial (Fin 3) ℕ).coeff
      (Finsupp.single 0 (K+1) + Finsupp.single 1 n + Finsupp.single 2 n) =
    (Multigraded.mixedPolynomial
      (firstGroup (κ := Fin K) (n := n)) secondGroup).coeff
…

Mentions: OAI.PermanentBorder.Multigraded.mixedPolynomial

lemma OAI.PermanentBorder.AmbientPolar.count_le_literal_coefficient line 49
Source documentation
A bound by the mixed coefficient is also a bound by the three-variable coefficient.
```
lemma count_le_literal_coefficient (K n D : ℕ)
    (h : D ≤ (Multigraded.mixedPolynomial
      (firstGroup (κ := Fin K) (n := n)) secondGroup).coeff
…
```
Mentions: OAI.PermanentBorder.Multigraded.mixedPolynomial