Integer matrices give linear forms. Composition is matrix multiplication, with an explicit coefficient-height bound.

@[reducible, inline]

noncomputable abbrev CCDN.integerLinearForm {σ : Type u_1} [Fintype σ] (a : σ → ℤ) : MvPolynomial σ ℚ

The rational linear form ∑ i, a i * X i with integer coefficient vector a.

Equations

• CCDN.integerLinearForm a = CCDN.linearForm fun (i : σ) => ↑(a i)

theorem CCDN.integerLinearForm_identity {σ : Type u_1} [Fintype σ] [DecidableEq σ] (i : σ) : (integerLinearForm fun (j : σ) => if j = i then 1 else 0) = MvPolynomial.X i

The integer linear form with the i-th standard basis vector as coefficients is X i.

theorem CCDN.integerLinearForm_comp {σ : Type u_1} {τ : Type u_2} [Fintype σ] [Fintype τ] (a : σ → ℤ) (b : σ → τ → ℤ) : (MvPolynomial.aeval fun (i : σ) => integerLinearForm (b i)) (integerLinearForm a) = integerLinearForm fun (j : τ) => ∑ i : σ, a i * b i j

Substituting the integer linear forms with coefficient rows b i into the integer linear form with coefficients a gives the integer linear form with coefficients ∑ i, a i * b i j, the product of the row vector a with the matrix b.

theorem CCDN.integerLinearForm_matrix_height {σ : Type u_1} {τ : Type u_2} [Fintype σ] (a : σ → ℤ) (b : σ → τ → ℤ) (H T : ℕ) (ha : ∀ (i : σ), |a i| ≤ ↑H) (hb : ∀ (i : σ) (j : τ), |b i j| ≤ ↑T) (j : τ) : |∑ i : σ, a i * b i j| ≤ ↑(Fintype.card σ) * ↑H * ↑T

If the entries of a are bounded by H and those of b by T in absolute value, then each entry of the product ∑ i, a i * b i j is bounded by Fintype.card σ * H * T.