Orthonormality of the executable Gram–Schmidt Q factor (Qᵀ Q = 1)

The columns of classical Gram–Schmidt's Q factor are identified with mathlib's normalized Gram–Schmidt vectors. Reading the columns of A as vectors of EuclideanSpace ℝ (Fin m), the j-th executable Q column equals Mathlib's gramSchmidtNormed ℝ of the column map (Qcol_bridge), so orthonormality follows from mathlib's gramSchmidtNormed_orthonormal'.

Main results

• Qcol_bridge: WithLp.toLp 2 (Qcol A k) = gramSchmidtNormed ℝ (gsCol A) k, so the executable Q column is Mathlib's normalized Gram–Schmidt vector, proved by strong induction on k.
• Q_orthonormal: dotFn (Qcol A a) (Qcol A b) = if a = b then 1 else 0 under positive R pivots.
• QT_mul_Q_eq_one and isQR_of_pos: the matrix-level Qᵀ Q = 1 and the full Spec.Factorization.IsQR predicate for the executable factors (combining with the reconstruction A = Q · R and R upper-triangular from the companion file).
• qrSpec_orthonormal: the tensor-level corollary.

Method

The bridge rests on three connectors over ℝ: dotFn = ⟪·,·⟫ and normFn = ‖·‖ on EuclideanSpace ℝ (Fin m), and the projection identity proj_normalize showing the un-normalized Gram–Schmidt projection term equals the normalized one. The strong induction feeds the partial identification of the earlier Q columns into gramSchmidt_def'', term by term.

Connectors between the executable scalar ops and the Euclidean inner product

theorem Spec.Factorization.Reconstruction.dotFn_eq_sum {p : ℕ} (u v : Fin p → ℝ) : dotFn u v = ∑ i : Fin p, u i * v i

dotFn as a Finset sum.

theorem Spec.Factorization.Reconstruction.dotFn_eq_inner {p : ℕ} (u v : Fin p → ℝ) : dotFn u v = inner ℝ (WithLp.toLp 2 u) (WithLp.toLp 2 v)

The executable dot product is the Euclidean inner product over ℝ.

theorem Spec.Factorization.Reconstruction.normFn_eq_norm {p : ℕ} (v : Fin p → ℝ) : normFn v = ‖WithLp.toLp 2 v‖

The executable Euclidean norm is the EuclideanSpace norm over ℝ.

theorem Spec.Factorization.Reconstruction.proj_normalize {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (w x : F) : (inner ℝ w x / ‖w‖ ^ 2) • w = inner ℝ (‖w‖⁻¹ • w) x • ‖w‖⁻¹ • w

The Gram–Schmidt projection term, with the normalized vector pulled out. Holds with no non-degeneracy hypothesis (both sides vanish when gramSchmidt = 0).

theorem Spec.Factorization.Reconstruction.gramSchmidtNormed_eq_inv_norm_smul {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : Fin n → F) (i : Fin n) : InnerProductSpace.gramSchmidtNormed ℝ f i = ‖InnerProductSpace.gramSchmidt ℝ f i‖⁻¹ • InnerProductSpace.gramSchmidt ℝ f i

gramSchmidtNormed over ℝ, with the scalar coercion removed.

theorem Spec.Factorization.Reconstruction.sum_Iio_eq_mask {n : ℕ} (k : Fin n) (h : Fin n → ℝ) : ∑ i < k, h i = ∑ i : Fin n, if ↑i < ↑k then h i else 0

A masked full sum equals the sum over Iio.

The bridge to Mathlib's gramSchmidt

noncomputable def Spec.Factorization.Reconstruction.gsCol {m n : ℕ} (A : Fin m → Fin n → ℝ) (j : Fin n) : EuclideanSpace ℝ (Fin m)

Column j of A as a vector of EuclideanSpace ℝ (Fin m).

theorem Spec.Factorization.Reconstruction.gsCol_apply {m n : ℕ} (A : Fin m → Fin n → ℝ) (k : Fin n) (r : Fin m) : (gsCol A k).ofLp r = gsA A k r

gsCol A k reads as the executable column gsA A k.

theorem Spec.Factorization.Reconstruction.gsV_bridge {m n : ℕ} (A : Fin m → Fin n → ℝ) (k : Fin n) (ih : ∀ (i : Fin n), ↑i < ↑k → WithLp.toLp 2 (Qcol A i) = InnerProductSpace.gramSchmidtNormed ℝ (gsCol A) i) : InnerProductSpace.gramSchmidt ℝ (gsCol A) k = WithLp.toLp 2 (gsV A (qsPrefix A k) k)

Given that the earlier Q columns coincide with mathlib's normalized Gram–Schmidt vectors, the executable orthogonalized vector v at index k equals Mathlib's (un-normalized) gramSchmidt vector.

theorem Spec.Factorization.Reconstruction.Qcol_bridge {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (k : Fin n) : WithLp.toLp 2 (Qcol A k) = InnerProductSpace.gramSchmidtNormed ℝ (gsCol A) k

The specification Q column at index k equals mathlib's gramSchmidtNormed, under positive R pivots.

Orthonormality Qᵀ Q = 1

theorem Spec.Factorization.Reconstruction.gramSchmidtNormed_gsCol_ne_zero {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (j : Fin n) : InnerProductSpace.gramSchmidtNormed ℝ (gsCol A) j ≠ 0

Each normalized Gram–Schmidt vector is non-zero (the pivot is positive).

theorem Spec.Factorization.Reconstruction.Q_orthonormal {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (a b : Fin n) : dotFn (Qcol A a) (Qcol A b) = if a = b then 1 else 0

Under positive R pivots, the specification Q columns satisfy qₐ · q_b = δₐᵦ.

theorem Spec.Factorization.Reconstruction.QT_mul_Q_eq_one {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) : ((Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k).transpose * Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k) = 1

Qᵀ Q = 1 for the specification Gram–Schmidt Q factor under positive pivots.

theorem Spec.Factorization.Reconstruction.isQR_of_pos {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) : IsQR (Matrix.of A) (Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k) (Matrix.of fun (k j : Fin n) => Rmat A k j)

For A with positive specification R-pivots, the Gram–Schmidt factors satisfy Spec.Factorization.IsQR: Qᵀ Q = 1, R upper-triangular, and A = Q · R.

theorem Spec.Factorization.Reconstruction.qrSpec_orthonormal {m n : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (hrank : ∀ (j : Fin n), 0 < get2 (qrRSpec A) j j) (a b : Fin n) : ∑ i : Fin m, get2 (qrQSpec A) i a * get2 (qrQSpec A) i b = if a = b then 1 else 0

For a tensor A with positive qrRSpec pivots, the Q factor qrQSpec A has orthonormal columns: Σ_i Q[i,a]·Q[i,b] = δₐᵦ.