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