Unit phases of positive matrix rescalings

Every nonzero complex number has a multiplicative unit-modulus part. Replacing a scalar that makes a matrix positive semidefinite by this unit phase preserves positive semidefiniteness. For a nonzero matrix, the unit phase with this property is unique.

theorem Complex.ne_zero_of_norm_eq_one {z : ℂ} (h : ‖z‖ = 1) : z ≠ 0

A complex scalar of unit norm is nonzero.

noncomputable def Complex.unitsPhase : ℂˣ →* Circle

The unit-modulus part of a nonzero complex number, as a multiplicative map.

Equations

• Complex.unitsPhase = { toFun := fun (z : ℂˣ) => ⟨↑z / ↑‖↑z‖, ⋯⟩, map_one' := Complex.unitsPhase._proof_3, map_mul' := Complex.unitsPhase._proof_5 }

noncomputable def Complex.phase (c : ℂ) (hc : c ≠ 0) : Circle

The unit-modulus part of a specified nonzero complex number.

Equations

• c.phase hc = Complex.unitsPhase (Units.mk0 c hc)

theorem Complex.phase_smul_posSemidef {n : Type u_1} [Finite n] {M : Matrix n n ℂ} {c : ℂ} (hc : c ≠ 0) (h : (c • M).PosSemidef) : (↑(c.phase hc) • M).PosSemidef

Replacing a nonzero rescaling scalar by its unit-modulus part preserves positive semidefiniteness.

theorem Circle.eq_of_smul_posSemidef {n : Type u_1} [Finite n] {M : Matrix n n ℂ} (hM : M ≠ 0) {u v : Circle} (hu : (↑u • M).PosSemidef) (hv : (↑v • M).PosSemidef) : u = v

A nonzero complex matrix admits at most one unit-modulus phase that makes it positive semidefinite.