FARMSAcceptedTheorem · Statement with omitted proof
Orthonormal matrices preserve Euclidean length
Multiplication by a matrix with orthonormal columns preserves the Euclidean norm.
Drineas & Mahoney ↗
Source label: thm:orthonormal-isometry
Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
Multiplication by a matrix with orthonormal columns preserves the Euclidean norm.
Assumptions & context
- V is real m × n, m ≥ n and VᵀV = I; x is an n-vector.
Source
Drineas & Mahoney. Lectures on randomized numerical linear algebra.
Source label: thm:orthonormal-isometry
02 / LEAN REPRESENTATION
Formal statement
Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.
theorem orthonormal_isometry (m n : ℕ) (x : Fin n → ℝ)
(V : Matrix (Fin m) (Fin n) ℝ) (hmn : n ≤ m) (hV : Vᵀ * V = 1) :
l2Norm (V *ᵥ x) = l2Norm x ∧ l2Norm (x ᵥ* Vᵀ) = l2Norm x := by
sorry
Complete Lean file and local definitions
import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity
open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal
namespace RNLAPhaseB.DM2017OrthonormalIsometry
/-- dm2017 thm:orthonormal-isometry. Given `x ∈ ℝ^n` and `V ∈ ℝ^{m×n}` with `m ≥ n`
and `Vᵀ V = I_n`, we have `‖V x‖₂ = ‖x‖₂` and `‖xᵀ Vᵀ‖₂ = ‖x‖₂`.
The vector 2-norm is the `p = 2` vector norm `(∑ |x_i|^2)^{1/2}`, realized by the
base's `l2Norm`. The row vector `xᵀ Vᵀ ∈ ℝ^{1×m}` is represented by its entries as
the vector-matrix product `x ᵥ* Vᵀ : Fin m → ℝ`; its 2-norm is the vector 2-norm of
those entries. -/
theorem orthonormal_isometry (m n : ℕ) (x : Fin n → ℝ)
(V : Matrix (Fin m) (Fin n) ℝ) (hmn : n ≤ m) (hV : Vᵀ * V = 1) :
l2Norm (V *ᵥ x) = l2Norm x ∧ l2Norm (x ᵥ* Vᵀ) = l2Norm x := by
sorry
end RNLAPhaseB.DM2017OrthonormalIsometry
How to read the formalization
- Both column-vector and row-vector formulations are retained.