This record groups the data and proof fields needed for “factorization”. A proposition-valued field is a requirement until a constructor supplies it. Actual factors together with the same two equations as 'ThinLQ'.
structure Factorization {m n : ℕ} (A : _root_.Matrix (Fin m) (Fin n) ℝ) (r : ℕ) where
R : _root_.Matrix (Fin m) (Fin r) ℝ
Q : _root_.Matrix (Fin r) (Fin n) ℝ
factorization : A = R * Q
orthogonal : Q * Q.transpose = 1
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “wide r”.
noncomputable def wideR {m n : ℕ} (hmn : m ≤ n)
(A : _root_.Matrix (Fin m) (Fin n) ℝ) : _root_.Matrix (Fin m) (Fin m) ℝ :=
fun i k => reduced A.transpose (Fin.castLE hmn k) i
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “wide q”.
noncomputable def wideQ {m n : ℕ} (hmn : m ≤ n)
(A : _root_.Matrix (Fin m) (Fin n) ℝ) : _root_.Matrix (Fin m) (Fin n) ℝ :=
fun k j => transform A.transpose (Fin.castLE hmn k) j
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “wide factorization”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem wide_factorization {m n : ℕ} (hmn : m ≤ n)
(A : _root_.Matrix (Fin m) (Fin n) ℝ) : A = wideR hmn A * wideQ hmn A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “wide orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem wide_orthogonal {m n : ℕ} (hmn : m ≤ n)
(A : _root_.Matrix (Fin m) (Fin n) ℝ) : wideQ hmn A * (wideQ hmn A).transpose = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “factor of le”. A deterministic wide-matrix supplier, including zero and repeated rows.
noncomputable def factorOfLE {m n : ℕ} (hmn : m ≤ n)
(A : _root_.Matrix (Fin m) (Fin n) ℝ) : Factorization A m where
R := wideR hmn A
Q := wideQ hmn A
factorization := wide_factorization hmn A
orthogonal := wide_orthogonal hmn A
/-- All shapes are handled by an explicit dimension comparison and recursion. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “factor”. All shapes are handled by an explicit dimension comparison and recursion.
noncomputable def factor {m n : ℕ} (A : _root_.Matrix (Fin m) (Fin n) ℝ) :
Factorization A (min m n) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “factor correct”; the hypotheses and conclusion in the code panel fix its exact scope. The concrete output satisfies the existing all-shape thin-LQ contract.
theorem factor_correct {m n : ℕ} (A : _root_.Matrix (Fin m) (Fin n) ℝ) :
A = (factor A).R * (factor A).Q ∧ (factor A).Q * (factor A).Q.transpose = 1 :=
⟨(factor A).factorization, (factor A).orthogonal⟩
commit-pinned source · Verso Blueprint panel