This definition gives the library's named construction or computation for “sweep”.
noncomputable def sweep {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(k : ℕ) : (remaining : ℕ) → k + remaining ≤ M →
_root_.Matrix (Fin N) (Fin M) ℝ
| 0, _ => A
| remaining + 1, columns =>
if h : k < N then
sweep (columnSweep A ⟨k, by omega⟩ k (N - 1 - k) (by omega))
(k + 1) remaining (by omega)
else sweep A (k + 1) remaining (by omega)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “sweep steps”.
noncomputable def sweepSteps {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(k : ℕ) : (remaining : ℕ) → k + remaining ≤ M → List (Step N)
| 0, _ => []
| remaining + 1, columns =>
if h : k < N then
columnSweepSteps A ⟨k, by omega⟩ k (N - 1 - k) (by omega) ++
sweepSteps (columnSweep A ⟨k, by omega⟩ k (N - 1 - k) (by omega))
(k + 1) remaining (by omega)
else sweepSteps A (k + 1) remaining (by omega)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sweep steps action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sweepSteps_action {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(k remaining : ℕ) (columns : k + remaining ≤ M) :
applySteps (sweepSteps A k remaining columns) A = sweep A k remaining columns := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “upper prefix”. Previously eliminated columns vanish strictly below their diagonal.
def UpperPrefix {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) (k : ℕ) : Prop :=
∀ col : Fin M, col.val < k → ∀ row : Fin N, col.val < row.val → A row col = 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep upper prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_upperPrefix {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (h : col.val < N) (fixedPrefix : UpperPrefix A col.val) :
UpperPrefix (columnSweep A col col.val (N - 1 - col.val) (by omega)) (col.val + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sweep upper prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sweep_upperPrefix {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(k remaining : ℕ) (columns : k + remaining ≤ M) (fixedPrefix : UpperPrefix A k) :
UpperPrefix (sweep A k remaining columns) (k + remaining) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sweep steps length le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sweepSteps_length_le {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(k remaining : ℕ) (columns : k + remaining ≤ M) :
(sweepSteps A k remaining columns).length ≤ N * remaining := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “steps matrix orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem stepsMatrix_orthogonal {N : ℕ} (steps : List (Step N)) :
(stepsMatrix steps).transpose * stepsMatrix steps = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “steps matrix det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem stepsMatrix_det {N : ℕ} (steps : List (Step N)) :
(stepsMatrix steps).det = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “decompose”.
noncomputable def decompose {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
List (Step N) := sweepSteps A 0 M (by omega)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “reduced”.
noncomputable def reduced {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
_root_.Matrix (Fin N) (Fin M) ℝ := sweep A 0 M (by omega)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “transform”.
noncomputable def transform {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
_root_.Matrix (Fin N) (Fin N) ℝ := stepsMatrix (decompose A)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “decompose action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem decompose_action {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
applySteps (decompose A) A = reduced A := sweepSteps_action A 0 M _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “transform mul”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem transform_mul {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
transform A * A = reduced A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “reduced zero below”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem reduced_zero_below {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(row : Fin N) (col : Fin M) (below : col.val < row.val) :
reduced A row col = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “decompose length le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem decompose_length_le {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
(decompose A).length ≤ N * M := sweepSteps_length_le A 0 M _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “transform orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem transform_orthogonal {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
(transform A).transpose * transform A = 1 := stepsMatrix_orthogonal _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “transform det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem transform_det {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
(transform A).det = 1 := stepsMatrix_det _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exact recovery”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem exact_recovery {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ) :
(transform A).transpose * reduced A = A := by
commit-pinned source · Verso Blueprint panel