AcceptedProposition · Statement with omitted proof

Unitary change of coordinates for a projector

Orthogonal projection transforms naturally under a unitary change of coordinates.

Halko, Martinsson & Tropp ↗
Source label: prop:conj-proj

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Orthogonal projection transforms naturally under a unitary change of coordinates.

U^*P_MU=P_{U^*M}

Assumptions & context

U is unitary and P_M projects onto the column space of M over the real or complex field.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:conj-proj

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem conjTranspose_mul_orthogonalProjector_mul_unitary
    {𝕜 : Type*} [RCLike 𝕜]
    {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (U : Matrix m m 𝕜) (M : Matrix m n 𝕜)
    (hU : U ∈ Matrix.unitaryGroup m 𝕜) :
    Uᴴ * orthogonalProjector M * U = orthogonalProjector (Uᴴ * M) := 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.HMTConjProj

/-- HMT, Proposition (prop:conj-proj): if `U` is unitary, then
`U^* P_M U = P_{U^* M}`.

Here `P_M` is the frozen base's `orthogonalProjector M`, the unique orthogonal
projector whose range is the column space of `M`. Unitarity of the square matrix
`U` is membership in Mathlib's `Matrix.unitaryGroup`, i.e. `U^* U = I` and
`U U^* = I`, with `U^*` the conjugate transpose. The scalar field is any
`RCLike` field, covering both the real and the complex settings. -/
theorem conjTranspose_mul_orthogonalProjector_mul_unitary
    {𝕜 : Type*} [RCLike 𝕜]
    {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (U : Matrix m m 𝕜) (M : Matrix m n 𝕜)
    (hU : U ∈ Matrix.unitaryGroup m 𝕜) :
    Uᴴ * orthogonalProjector M * U = orthogonalProjector (Uᴴ * M) := by
  sorry

end RNLAPhaseB.HMTConjProj

How to read the formalization

The projector is constructed from the column space rather than supplied as an arbitrary matrix.

← Back to all statements