This definition gives the library's named construction or computation for “prefix columns”. The first 'k' rectangular columns are their corresponding coordinate vectors.
def PrefixColumns {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r ≤ N) (k : ℕ) : Prop :=
∀ col : Fin r, col.val < k → ∀ row : Fin N,
V row col = if row = Fin.castLE hr col then 1 else 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rotate rows isometry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rotateRows_isometry {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hV : V.transpose * V = 1) (i j : Fin N) (hij : i ≠ j) (theta : ℝ) :
(rotateRows V i j theta).transpose * rotateRows V i j theta = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep isometry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_isometry {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hV : V.transpose * V = 1) (col : Fin r) (lo count : ℕ) (bound : lo + count < N) :
(columnSweep V col lo count bound).transpose * columnSweep V col lo count bound = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “zero of fixed column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem zero_of_fixed_column {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r ≤ N) (hV : V.transpose * V = 1) (old col : Fin r) (different : old ≠ col)
(fixed : ∀ row, V row old = if row = Fin.castLE hr old then 1 else 0) :
V (Fin.castLE hr old) col = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_prefix {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r ≤ N) (col : Fin r) (count : ℕ) (bound : col.val + count < N)
(fixed : PrefixColumns V hr col.val) :
PrefixColumns (columnSweep V col col.val count bound) hr col.val := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “supported column sq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem supported_column_sq {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r ≤ N) (hV : V.transpose * V = 1) (col : Fin r)
(support : ∀ row, row ≠ Fin.castLE hr col → V row col = 0) :
V (Fin.castLE hr col) col ^ 2 = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep prefix succ”; the hypotheses and conclusion in the code panel fix its exact scope. A nonfinal rectangular isometry column is swept to a positive unit pivot.
theorem columnSweep_prefix_succ {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r ≤ N) (hV : V.transpose * V = 1) (col : Fin r) (count : ℕ)
(dimension : col.val + count + 1 = N) (positive : 0 < count)
(fixed : PrefixColumns V hr col.val) :
PrefixColumns (columnSweep V col col.val count (by omega)) hr (col.val + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sweep prefix”; the hypotheses and conclusion in the code panel fix its exact scope. The shared rectangular sweep fixes every processed isometry column.
theorem sweep_prefix {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r < N) (hV : V.transpose * V = 1)
(k remaining : ℕ) (columns : k + remaining ≤ r) (fixed : PrefixColumns V hr.le k) :
PrefixColumns (RectangularGivens.sweep V k remaining columns) hr.le (k + remaining) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “reduced prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem reduced_prefix {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r < N) (hV : V.transpose * V = 1) :
PrefixColumns (RectangularGivens.reduced V) hr.le r := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “prefix completion”. Inverse of the explicitly computed row rotations; no matrix witness is chosen.
noncomputable def prefixCompletion {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ) :
_root_.Matrix (Fin N) (Fin N) ℝ := (RectangularGivens.transform V).transpose
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prefix completion orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prefixCompletion_orthogonal {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ) :
(prefixCompletion V).transpose * prefixCompletion V = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prefix completion det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prefixCompletion_det {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ) :
(prefixCompletion V).det = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prefix completion columns”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prefixCompletion_columns {N r : ℕ} (V : _root_.Matrix (Fin N) (Fin r) ℝ)
(hr : r < N) (hV : V.transpose * V = 1) (row : Fin N) (col : Fin r) :
prefixCompletion V row (Fin.castLE hr.le col) = V row col := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “extend prefix”. Greedy swaps deterministically extend a finite prefix injection.
def extendPrefix {N r : ℕ} (hr : r ≤ N) (e : Fin r ↪ Fin N) :
(k : ℕ) → k ≤ r → Equiv.Perm (Fin N)
| 0, _ => Equiv.refl _
| k + 1, hk =>
let p := extendPrefix hr e k (by omega)
p.trans (Equiv.swap (p ⟨k, by omega⟩) (e ⟨k, by omega⟩))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “extend prefix agrees”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem extendPrefix_agrees {N r : ℕ} (hr : r ≤ N) (e : Fin r ↪ Fin N)
(k : ℕ) (hk : k ≤ r) (a : Fin r) (ha : a.val < k) :
extendPrefix hr e k hk (Fin.castLE hr a) = e a := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “unused position”. The first unused original coordinate is carried to an unused physical label.
def unusedPosition {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N) : Fin N :=
extendPrefix hr.le e r le_rfl ⟨r, hr⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “unused position ne”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem unusedPosition_ne {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N) (a : Fin r) :
e a ≠ unusedPosition hr e := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “permute columns”. Send original column 'a' to physical column 'p a'.
def permuteColumns {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(p : Equiv.Perm (Fin N)) : _root_.Matrix (Fin N) (Fin N) ℝ :=
U.submatrix id p.symm
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “permute columns apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem permuteColumns_apply {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(p : Equiv.Perm (Fin N)) (row col : Fin N) :
permuteColumns U p row (p col) = U row col := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “permute columns orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem permuteColumns_orthogonal {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(hU : U.transpose * U = 1) (p : Equiv.Perm (Fin N)) :
(permuteColumns U p).transpose * permuteColumns U p = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “permute columns det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem permuteColumns_det {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(p : Equiv.Perm (Fin N)) :
(permuteColumns U p).det = (Equiv.Perm.sign p : ℤ) * U.det := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “orient columns”. Correct only an unused column, using finite permutation parity, not a determinant test.
noncomputable def orientColumns {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(p : Equiv.Perm (Fin N)) (unused : Fin N) : _root_.Matrix (Fin N) (Fin N) ℝ :=
if Equiv.Perm.sign p = 1 then permuteColumns U p
else permuteColumns U p * RealIsometryCompletion.signFlip unused
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “orient columns orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem orientColumns_orthogonal {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(hU : U.transpose * U = 1) (p : Equiv.Perm (Fin N)) (unused : Fin N) :
(orientColumns U p unused).transpose * orientColumns U p unused = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “orient columns det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem orientColumns_det {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(hU : U.det = 1) (p : Equiv.Perm (Fin N)) (unused : Fin N) :
(orientColumns U p unused).det = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “orient columns preserves”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem orientColumns_preserves {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(p : Equiv.Perm (Fin N)) (unused row col : Fin N) (hcol : p col ≠ unused) :
orientColumns U p unused row (p col) = U row col := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “place columns”. Explicit physical-column placement of a prefix SO completion.
noncomputable def placeColumns {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N)
(U : _root_.Matrix (Fin N) (Fin N) ℝ) : _root_.Matrix (Fin N) (Fin N) ℝ :=
orientColumns U (extendPrefix hr.le e r le_rfl) (unusedPosition hr e)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “place columns spec”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem placeColumns_spec {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N)
(U : _root_.Matrix (Fin N) (Fin N) ℝ) (hU : U.transpose * U = 1) (hd : U.det = 1) :
(placeColumns hr e U).transpose * placeColumns hr e U = 1 ∧
(placeColumns hr e U).det = 1 ∧
∀ row a, placeColumns hr e U row (e a) = U row (Fin.castLE hr.le a) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “complete”. Actual deterministic SO matrix with columns at the prescribed physical positions.
noncomputable def complete {N r : ℕ} (hr : r < N)
(V : _root_.Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N) :
_root_.Matrix (Fin N) (Fin N) ℝ := placeColumns hr e (prefixCompletion V)
/-- The supplied hypothesis is only the input column isometry; the returned
matrix is computed by the named producer, not supplied or selected existentially. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “complete spec”; the hypotheses and conclusion in the code panel fix its exact scope. The supplied hypothesis is only the input column isometry; the returned matrix is computed by the named producer, not supplied or selected existentially.
theorem complete_spec {N r : ℕ} (hr : r < N)
(V : _root_.Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N)
(hV : V.transpose * V = 1) :
(complete hr V e).transpose * complete hr V e = 1 ∧
(complete hr V e).det = 1 ∧ ∀ row a, complete hr V e row (e a) = V row a := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “complete named”. Transport using a supplied explicit coordinate equivalence, not an arbitrary enumeration chosen for the named basis.
noncomputable def completeNamed {I : Type*} [Fintype I] [DecidableEq I] {N r : ℕ}
(coordinates : I ≃ Fin N) (hr : r < N)
(V : _root_.Matrix I (Fin r) ℝ) (e : Fin r ↪ I) : _root_.Matrix I I ℝ :=
_root_.Matrix.reindex coordinates.symm coordinates.symm
(complete hr (V.submatrix coordinates.symm id) (e.trans coordinates.toEmbedding))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “complete named spec”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem completeNamed_spec {I : Type*} [Fintype I] [DecidableEq I] {N r : ℕ}
(coordinates : I ≃ Fin N) (hr : r < N)
(V : _root_.Matrix I (Fin r) ℝ) (e : Fin r ↪ I) (hV : V.transpose * V = 1) :
(completeNamed coordinates hr V e).transpose * completeNamed coordinates hr V e = 1 ∧
(completeNamed coordinates hr V e).det = 1 ∧
∀ row a, completeNamed coordinates hr V e row (e a) = V row a := by
commit-pinned source · Verso Blueprint panel