Mathlib-side correspondence lemmas for hex-gram-schmidt.

This module converts dense Hex.Matrix rows into the finite-dimensional real vector space used by Mathlib's gramSchmidt, then states the rowwise correspondence between the executable Hex.GramSchmidt basis and Mathlib's orthogonalization process.

def Hex.GramSchmidtMathlib.rowToEuclidean {m : ℕ} (row : Vector ℚ m) : EuclideanSpace ℝ (Fin m)

View a rational dense row as a vector in Mathlib's standard Euclidean space on Fin m.

Equations

• Hex.GramSchmidtMathlib.rowToEuclidean row = WithLp.toLp 2 fun (j : Fin m) => ↑row[j]

@[simp]

theorem Hex.GramSchmidtMathlib.rowToEuclidean_apply {m : ℕ} (row : Vector ℚ m) (j : Fin m) : (rowToEuclidean row).ofLp j = ↑row[j]

Coordinate access commutes with rowToEuclidean: the j-th component of the converted vector is the real cast of the j-th rational entry.

@[simp]

theorem Hex.GramSchmidtMathlib.rowToEuclidean_zero {m : ℕ} : rowToEuclidean 0 = 0

rowToEuclidean sends the zero row to the zero vector.

@[simp]

theorem Hex.GramSchmidtMathlib.rowToEuclidean_add {m : ℕ} (a b : Vector ℚ m) : rowToEuclidean (a + b) = rowToEuclidean a + rowToEuclidean b

rowToEuclidean is additive: it sends a rowwise sum to the sum of converted vectors.

@[simp]

theorem Hex.GramSchmidtMathlib.rowToEuclidean_sub {m : ℕ} (a b : Vector ℚ m) : rowToEuclidean (a - b) = rowToEuclidean a - rowToEuclidean b

rowToEuclidean commutes with subtraction.

@[simp]

theorem Hex.GramSchmidtMathlib.rowToEuclidean_smul {m : ℕ} (c : ℚ) (row : Vector ℚ m) : rowToEuclidean (c • row) = ↑c • rowToEuclidean row

rowToEuclidean is rational-linear: it sends a rational scalar multiple to the corresponding real scalar multiple of the converted vector.

def Hex.GramSchmidtMathlib.castIntMatrix {n m : ℕ} (b : Matrix ℤ n m) : Matrix ℚ n m

Cast an integer dense matrix into the rational matrix space of HexGramSchmidt.

Equations

• Hex.GramSchmidtMathlib.castIntMatrix b = { data := Vector.map (fun (row : Vector ℤ m) => Vector.map (fun (x : ℤ) => ↑x) row) b.rows }

def Hex.GramSchmidtMathlib.ratRowFamily {n m : ℕ} (b : Matrix ℚ n m) : Fin n → EuclideanSpace ℝ (Fin m)

The row family fed to Mathlib's gramSchmidt for a rational matrix.

Equations

• Hex.GramSchmidtMathlib.ratRowFamily b i = Hex.GramSchmidtMathlib.rowToEuclidean (b.row i)

def Hex.GramSchmidtMathlib.intRowFamily {n m : ℕ} (b : Matrix ℤ n m) : Fin n → EuclideanSpace ℝ (Fin m)

The row family fed to Mathlib's gramSchmidt for an integer matrix.

Equations

• Hex.GramSchmidtMathlib.intRowFamily b = Hex.GramSchmidtMathlib.ratRowFamily (Hex.GramSchmidtMathlib.castIntMatrix b)

theorem Hex.GramSchmidtMathlib.rowToEuclidean_inner {m : ℕ} (a b : Vector ℚ m) : inner ℝ (rowToEuclidean a) (rowToEuclidean b) = ↑(a.dotProduct b)

Mathlib's real inner product on converted rows agrees with the executable rational dense dot product after casting to ℝ.

theorem Hex.GramSchmidtMathlib.rat_coeffs_lower_projection_real {n m : ℕ} (b : Matrix ℚ n m) {i j : Fin n} (hji : ↑j < ↑i) : ↑(GramSchmidt.entry (GramSchmidt.Rat.coeffs b) i j) = inner ℝ (rowToEuclidean ((GramSchmidt.Rat.basis b).row j)) (rowToEuclidean (b.row i)) / ‖rowToEuclidean ((GramSchmidt.Rat.basis b).row j)‖ ^ 2

A strictly lower executable coefficient agrees, after casting to ℝ, with Mathlib's projection coefficient for the corresponding converted rows.

theorem Hex.GramSchmidtMathlib.rat_basis_row_eq_gramSchmidt {n m : ℕ} (b : Matrix ℚ n m) (i : Fin n) : rowToEuclidean ((GramSchmidt.Rat.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (ratRowFamily b) i

The rational Gram-Schmidt basis agrees rowwise with Mathlib's real-valued gramSchmidt after coercing coefficients into ℝ.

theorem Hex.GramSchmidtMathlib.int_basis_row_eq_gramSchmidt {n m : ℕ} (b : Matrix ℤ n m) (i : Fin n) : rowToEuclidean ((GramSchmidt.Int.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (intRowFamily b) i

The integer Gram-Schmidt basis agrees rowwise with Mathlib's real-valued gramSchmidt after coercing coefficients into ℝ.