hex

5.3. Key correctness theorems🔗

The defining guarantee is orthogonality: distinct basis rows have zero dot product. The statement is given over both the rational and the integer input (the latter taken in Rat).

🔗theorem
Hex.GramSchmidt.Rat.basis_orthogonal {n m : Nat}
  (b : Hex.Matrix Rat n m) (i j : Nat) (hi : i < n) (hj : j < n)
  (hij : i ≠ j) :
  ((Hex.GramSchmidt.Rat.basis b).row ⟨i, hi⟩).dotProduct
      ((Hex.GramSchmidt.Rat.basis b).row ⟨j, hj⟩) =
    0
Hex.GramSchmidt.Rat.basis_orthogonal
  {n m : Nat} (b : Hex.Matrix Rat n m)
  (i j : Nat) (hi : i < n) (hj : j < n)
  (hij : i ≠ j) :
  ((Hex.GramSchmidt.Rat.basis b).row
          ⟨i, hi⟩).dotProduct
      ((Hex.GramSchmidt.Rat.basis b).row
        ⟨j, hj⟩) =
    0

The defining guarantee of the construction: distinct rational Gram-Schmidt basis rows are mutually orthogonal (their dot product is zero).

🔗theorem
Hex.GramSchmidt.Int.basis_orthogonal {n m : Nat}
  (b : Hex.Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n)
  (hij : i ≠ j) :
  ((Hex.GramSchmidt.Int.basis b).row ⟨i, hi⟩).dotProduct
      ((Hex.GramSchmidt.Int.basis b).row ⟨j, hj⟩) =
    0
Hex.GramSchmidt.Int.basis_orthogonal
  {n m : Nat} (b : Hex.Matrix Int n m)
  (i j : Nat) (hi : i < n) (hj : j < n)
  (hij : i ≠ j) :
  ((Hex.GramSchmidt.Int.basis b).row
          ⟨i, hi⟩).dotProduct
      ((Hex.GramSchmidt.Int.basis b).row
        ⟨j, hj⟩) =
    0

Distinct Gram-Schmidt basis rows of an integer matrix (taken in Rat) are mutually orthogonal.

The basis and coefficient matrices together factor the input. Each input row equals its orthogonalized basis row plus the coefficient-weighted combination of the earlier basis rows: the triangular factorization b = coeffs · basis, stated row by row.

🔗theorem
Hex.GramSchmidt.Rat.basis_decomposition {n m : Nat}
  (b : Hex.Matrix Rat n m) (i : Nat) (hi : i < n) :
  b.row ⟨i, hi⟩ =
    (Hex.GramSchmidt.Rat.basis b).row ⟨i, hi⟩ +
      Hex.GramSchmidt.prefixCombination (Hex.GramSchmidt.Rat.coeffs b)
        (Hex.GramSchmidt.Rat.basis b) i hi
Hex.GramSchmidt.Rat.basis_decomposition
  {n m : Nat} (b : Hex.Matrix Rat n m)
  (i : Nat) (hi : i < n) :
  b.row ⟨i, hi⟩ =
    (Hex.GramSchmidt.Rat.basis b).row
        ⟨i, hi⟩ +
      Hex.GramSchmidt.prefixCombination
        (Hex.GramSchmidt.Rat.coeffs b)
        (Hex.GramSchmidt.Rat.basis b) i hi

The triangular factorization b = coeffs · basis, stated row by row: each rational input row equals its orthogonalized basis row plus the coefficient-weighted combination of the earlier basis rows.

🔗theorem
Hex.GramSchmidt.Int.basis_decomposition {n m : Nat}
  (b : Hex.Matrix Int n m) (i : Nat) (hi : i < n) :
  Vector.map (fun x => ↑x) (b.row ⟨i, hi⟩) =
    (Hex.GramSchmidt.Int.basis b).row ⟨i, hi⟩ +
      Hex.GramSchmidt.prefixCombination (Hex.GramSchmidt.Int.coeffs b)
        (Hex.GramSchmidt.Int.basis b) i hi
Hex.GramSchmidt.Int.basis_decomposition
  {n m : Nat} (b : Hex.Matrix Int n m)
  (i : Nat) (hi : i < n) :
  Vector.map (fun x => ↑x)
      (b.row ⟨i, hi⟩) =
    (Hex.GramSchmidt.Int.basis b).row
        ⟨i, hi⟩ +
      Hex.GramSchmidt.prefixCombination
        (Hex.GramSchmidt.Int.coeffs b)
        (Hex.GramSchmidt.Int.basis b) i hi

The triangular factorization for an integer matrix: each input row, cast into Rat, equals its orthogonalized basis row plus the coefficient-weighted combination of the earlier basis rows.

The coefficient matrix is lower-unitriangular, and its strictly lower entries are exactly the projection coefficients of the input row onto the earlier basis row.

🔗theorem
Hex.GramSchmidt.Rat.coeffs_diag {n m : Nat} (b : Hex.Matrix Rat n m)
  (i : Nat) (hi : i < n) :
  Hex.GramSchmidt.entry (Hex.GramSchmidt.Rat.coeffs b) ⟨i, hi⟩ ⟨i, hi⟩ =
    1
Hex.GramSchmidt.Rat.coeffs_diag
  {n m : Nat} (b : Hex.Matrix Rat n m)
  (i : Nat) (hi : i < n) :
  Hex.GramSchmidt.entry
      (Hex.GramSchmidt.Rat.coeffs b)
      ⟨i, hi⟩ ⟨i, hi⟩ =
    1

The rational coefficient matrix has unit diagonal: each input row enters its own decomposition with weight 1.

🔗theorem
Hex.GramSchmidt.Rat.coeffs_upper {n m : Nat} (b : Hex.Matrix Rat n m)
  (i j : Nat) (hi : i < n) (hj : j < n) (hij : i < j) :
  Hex.GramSchmidt.entry (Hex.GramSchmidt.Rat.coeffs b) ⟨i, hi⟩ ⟨j, hj⟩ =
    0
Hex.GramSchmidt.Rat.coeffs_upper
  {n m : Nat} (b : Hex.Matrix Rat n m)
  (i j : Nat) (hi : i < n) (hj : j < n)
  (hij : i < j) :
  Hex.GramSchmidt.entry
      (Hex.GramSchmidt.Rat.coeffs b)
      ⟨i, hi⟩ ⟨j, hj⟩ =
    0

The rational coefficient matrix is lower triangular: entries strictly above the diagonal vanish, since a row only combines basis rows with smaller index.

🔗theorem
Hex.GramSchmidt.Rat.coeffs_lower_projection {n m : Nat}
  (b : Hex.Matrix Rat n m) {i j : Fin n} (hji : ↑j < ↑i) :
  Hex.GramSchmidt.entry (Hex.GramSchmidt.Rat.coeffs b) i j =
    if
        ((Hex.GramSchmidt.Rat.basis b).row j).dotProduct
            ((Hex.GramSchmidt.Rat.basis b).row j) =
          0 then
      0
    else
      (b.row i).dotProduct ((Hex.GramSchmidt.Rat.basis b).row j) /
        ((Hex.GramSchmidt.Rat.basis b).row j).dotProduct
          ((Hex.GramSchmidt.Rat.basis b).row j)
Hex.GramSchmidt.Rat.coeffs_lower_projection
  {n m : Nat} (b : Hex.Matrix Rat n m)
  {i j : Fin n} (hji : ↑j < ↑i) :
  Hex.GramSchmidt.entry
      (Hex.GramSchmidt.Rat.coeffs b) i j =
    if
        ((Hex.GramSchmidt.Rat.basis b).row
                j).dotProduct
            ((Hex.GramSchmidt.Rat.basis
                  b).row
              j) =
          0 then
      0
    else
      (b.row i).dotProduct
          ((Hex.GramSchmidt.Rat.basis
                b).row
            j) /
        ((Hex.GramSchmidt.Rat.basis b).row
              j).dotProduct
          ((Hex.GramSchmidt.Rat.basis
                b).row
            j)

Strictly lower-triangular coefficient entries are the rational projection coefficient of the input row onto the earlier generated basis row.