Quadratic forms: definitions

• quadForm M x: the quadratic form x ↦ xᵀ M x of a square matrix M, and quadFormPolynomial M, the same form as a polynomial ∑ᵢ ∑ⱼ M i j Xᵢ Xⱼ.
• hankelCauchyZMod q N: the N × N matrix over ZMod q with entries 1 / (i + j + 2). It is the Cauchy matrix cauchy x y with nodes x i = i + 1 and y j = -(j + 1), and it is symmetric.
• hankelCauchyCharZero F N: the matrix with the same entries 1 / (i + j + 2) over a field F, totally regular when F has characteristic zero.

def Algebraic.Cutwidth.MultiOutput.quadForm {F : Type u_1} [CommRing F] {N : ℕ} (M : Matrix (Fin N) (Fin N) F) (x : Fin N → F) : F

The quadratic form x ↦ xᵀ M x of a square matrix M.

Equations

• Algebraic.Cutwidth.MultiOutput.quadForm M x = x ⬝ᵥ M.mulVec x

noncomputable def Algebraic.Cutwidth.MultiOutput.quadFormPolynomial {K : Type u_1} [CommSemiring K] {N : ℕ} (M : Matrix (Fin N) (Fin N) K) : MvPolynomial (Fin N) K

The quadratic form of M as a polynomial, ∑ᵢ ∑ⱼ M i j Xᵢ Xⱼ.

Equations

• Algebraic.Cutwidth.MultiOutput.quadFormPolynomial M = ∑ i : Fin N, ∑ j : Fin N, MvPolynomial.C (M i j) * (MvPolynomial.X i * MvPolynomial.X j)

def Algebraic.Cutwidth.MultiOutput.hankelCauchyZMod (q N : ℕ) : Matrix (Fin N) (Fin N) (ZMod q)

The N × N Hankel Cauchy matrix over ZMod q with entries 1 / (i + j + 2) for 0 ≤ i, j < N. For a prime q > 2 N it is the Cauchy matrix with nodes x i = i + 1 and y j = -(j + 1).

Equations

• Algebraic.Cutwidth.MultiOutput.hankelCauchyZMod q N = Matrix.of fun (i j : Fin N) => (↑(↑i + ↑j + 2))⁻¹

def Algebraic.Cutwidth.MultiOutput.hankelCauchyCharZero (F : Type u_1) [Field F] (N : ℕ) : Matrix (Fin N) (Fin N) F

The N × N Hankel Cauchy matrix over a field F, with entries 1 / (i + j + 2) for 0 ≤ i, j < N. In characteristic zero it is the Cauchy matrix with nodes x i = i + 1 and y j = -(j + 1).

Equations

• Algebraic.Cutwidth.MultiOutput.hankelCauchyCharZero F N = Matrix.of fun (i j : Fin N) => (↑(↑i + ↑j + 2))⁻¹