The Cayley transform

cayley S = (1 - S) * (1 + S)⁻¹ maps skew-Hermitian matrices to unitaries, and every unitary U for which 1 + U is invertible is cayley S for the skew-Hermitian S = (1 - U) * (1 + U)⁻¹; multiplying U by a suitable unit scalar z always makes 1 + z • U invertible, and (z • U) P (z • U)ᴴ = U P Uᴴ, so up to a phase every unitary is a Cayley transform. This is the parametrization of unitaries by which the enumeration of lem:value-lower-approx reaches exact unitaries with Gaussian-rational entries: the Cayley transform of a skew-Hermitian matrix with Gaussian-rational entries has Gaussian-rational entries, and the transform is 2-Lipschitz (MIPRE.Foundations.ValueApprox.Norms), so rounding S entrywise approximates U.

The one analytic input is IsSkewHermitian.mulVec_one_add_eq_zero: for skew-Hermitian S, ⟨v, S v⟩ is purely imaginary, so (1 + S) v = 0 forces v = 0.

def MIPRE.ValueApprox.IsSkewHermitian {n : Type u_1} (S : Matrix n n ℂ) : Prop

Skew-Hermitian matrices: Sᴴ = -S.

Equations

• MIPRE.ValueApprox.IsSkewHermitian S = (S.conjTranspose = -S)

theorem MIPRE.ValueApprox.IsSkewHermitian.neg {n : Type u_1} {S : Matrix n n ℂ} (hS : IsSkewHermitian S) : IsSkewHermitian (-S)

theorem MIPRE.ValueApprox.IsSkewHermitian.zero {n : Type u_1} : IsSkewHermitian 0

theorem MIPRE.ValueApprox.IsSkewHermitian.re_dotProduct_mulVec {n : Type u_1} {S : Matrix n n ℂ} [Fintype n] (hS : IsSkewHermitian S) (v : n → ℂ) : (star v ⬝ᵥ S.mulVec v).re = 0

The quadratic form of a skew-Hermitian matrix is purely imaginary.

theorem MIPRE.ValueApprox.IsSkewHermitian.mulVec_one_add_eq_zero {n : Type u_1} {S : Matrix n n ℂ} [Fintype n] [DecidableEq n] (hS : IsSkewHermitian S) {v : n → ℂ} (h : (1 + S).mulVec v = 0) : v = 0

(1 + S) v = 0 forces v = 0, since ‖(1 + S) v‖² = ‖v‖² + ‖S v‖².

theorem MIPRE.ValueApprox.IsSkewHermitian.isUnit_one_add {n : Type u_1} {S : Matrix n n ℂ} [Fintype n] [DecidableEq n] (hS : IsSkewHermitian S) : IsUnit (1 + S)

theorem MIPRE.ValueApprox.IsSkewHermitian.isUnit_one_sub {n : Type u_1} {S : Matrix n n ℂ} [Fintype n] [DecidableEq n] (hS : IsSkewHermitian S) : IsUnit (1 - S)

noncomputable def MIPRE.ValueApprox.cayley {n : Type u_1} [Fintype n] [DecidableEq n] (S : Matrix n n ℂ) : Matrix n n ℂ

The Cayley transform (1 - S) * (1 + S)⁻¹.

Equations

• MIPRE.ValueApprox.cayley S = (1 - S) * (1 + S)⁻¹

theorem MIPRE.ValueApprox.cayley_eq {n : Type u_1} [Fintype n] [DecidableEq n] {S : Matrix n n ℂ} (h : IsUnit (1 + S)) : cayley S = 2 • (1 + S)⁻¹ - 1

cayley S = 2 (1 + S)⁻¹ - 1 whenever 1 + S is invertible.

theorem MIPRE.ValueApprox.cayley_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] {S : Matrix n n ℂ} (hS : IsSkewHermitian S) : cayley S ∈ Matrix.unitaryGroup n ℂ

The Cayley transform of a skew-Hermitian matrix is unitary.

theorem MIPRE.ValueApprox.exists_isSkewHermitian_cayley_eq {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (h1 : IsUnit (1 + U)) : ∃ (S : Matrix n n ℂ), IsSkewHermitian S ∧ cayley S = U

Every unitary U with 1 + U invertible is the Cayley transform of the skew-Hermitian matrix (1 - U) * (1 + U)⁻¹.

Phases

cayley reaches only the unitaries U with 1 + U invertible. Multiplying U by a unit scalar z does not change the conjugation P ↦ U P Uᴴ, and some unit z always makes 1 + z • U invertible: z ↦ det (1 + z • U) is a polynomial with constant term 1.

theorem MIPRE.ValueApprox.smul_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) {z : ℂ} (hz : ‖z‖ = 1) : z • U ∈ Matrix.unitaryGroup n ℂ

z • U is unitary when U is and ‖z‖ = 1.

theorem MIPRE.ValueApprox.smul_mul_mul_conjTranspose_smul {n : Type u_1} [Fintype n] (U P : Matrix n n ℂ) {z : ℂ} (hz : ‖z‖ = 1) : z • U * P * (z • U).conjTranspose = U * P * U.conjTranspose

Conjugating by z • U for a unit scalar z is conjugating by U.

theorem MIPRE.ValueApprox.infinite_setOf_norm_eq_one : {z : ℂ | ‖z‖ = 1}.Infinite

The unit circle is infinite: m ↦ (1 + m i) / (1 - m i) is injective on ℕ.

theorem MIPRE.ValueApprox.exists_norm_eq_one_isUnit_one_add_smul {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℂ) : ∃ (z : ℂ), ‖z‖ = 1 ∧ IsUnit (1 + z • U)

Some unit scalar multiple z • U of any matrix has 1 + z • U invertible: det (1 + z • U) is a polynomial in z with constant term 1, so it has finitely many roots, while the unit circle is infinite.