Real powers of positive definite matrices

This file restores the upstream monlib4 API for real powers of positive semidefinite and positive definite matrices. The definitions are stated in terms of the current Mathlib Hermitian spectral theorem.

theorem Matrix.IsHermitian.eigenvectorMatrix_conjTranspose_mul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : hA.eigenvectorMatrix.conjTranspose * hA.eigenvectorMatrix = 1

noncomputable def Matrix.IsHermitian.rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.IsHermitian) (r : ℝ) : Matrix n n 𝕜

Real powers of a Hermitian matrix, defined by spectral calculus.

Equations

• hQ.rpow r = (Matrix.innerAut hQ.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ (hQ.eigenvalues ^ r)))

@[reducible, inline]

noncomputable abbrev Matrix.PosSemidef.rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) (r : ℝ) : Matrix n n 𝕜

Real powers of a positive semidefinite matrix.

Equations

• hQ.rpow r = ⋯.rpow r

@[reducible, inline]

noncomputable abbrev Matrix.PosDef.rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) : Matrix n n 𝕜

Real powers of a positive definite matrix.

Equations

• hQ.rpow r = ⋯.rpow r

theorem Matrix.PosDef.rpow_eq {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) : hQ.rpow r = (Matrix.innerAut ⋯.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ (⋯.eigenvalues ^ r)))

theorem Matrix.PosSemidef.rpow_mul_rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (r₁ r₂ : NNRealˣ) {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) : hQ.rpow ↑↑r₁ * hQ.rpow ↑↑r₂ = hQ.rpow (↑↑r₁ + ↑↑r₂)

theorem Matrix.PosDef.rpow_mul_rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (r₁ r₂ : ℝ) {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : hQ.rpow r₁ * hQ.rpow r₂ = hQ.rpow (r₁ + r₂)

theorem Matrix.IsHermitian.rpow_one_eq_self {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.IsHermitian) : hQ.rpow 1 = Q

theorem Matrix.PosSemidef.rpow_one_eq_self {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) : hQ.rpow 1 = Q

theorem Matrix.PosDef.rpow_one_eq_self {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : hQ.rpow 1 = Q

@[reducible]

noncomputable instance Matrix.PosDef.eigenvaluesInvertible {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : Invertible ⋯.eigenvalues

Equations

• hQ.eigenvaluesInvertible = { invOf := ⋯.eigenvalues⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[reducible]

noncomputable instance Matrix.PosDef.eigenvaluesInvertible' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : Invertible (RCLike.ofReal ∘ ⋯.eigenvalues)

Equations

• hQ.eigenvaluesInvertible' = { invOf := RCLike.ofReal ∘ ⋯.eigenvalues⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem Matrix.PosDef.rpow_neg_one_eq_inv_self {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : hQ.rpow (-1) = Q⁻¹

theorem Matrix.IsHermitian.rpow_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.IsHermitian) : hQ.rpow 0 = 1

theorem Matrix.PosSemidef.rpow_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) : hQ.rpow 0 = 1

theorem Matrix.PosDef.rpow_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : hQ.rpow 0 = 1

theorem Matrix.IsHermitian.rpow.isHermitian {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.IsHermitian) (r : ℝ) : (hQ.rpow r).IsHermitian

theorem Matrix.PosSemidef.rpow.isPosSemidef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) (r : ℝ) : (hQ.rpow r).PosSemidef

theorem Matrix.PosDef.rpow.isPosDef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) : (hQ.rpow r).PosDef

theorem Matrix.PosSemidef.sqrt_eq_rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) : CFC.sqrt Q = hQ.rpow (1 / 2)

theorem Matrix.PosDef.sqrt_eq_rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : CFC.sqrt Q = hQ.rpow (1 / 2)

theorem Matrix.PosDef.rpow_ne_zero {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {Q : Matrix n n ℂ} (hQ : Q.PosDef) {r : ℝ} : hQ.rpow r ≠ 0

theorem Matrix.IsHermitian.rpow_cast {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.IsHermitian) (r : ℝ) {S : Matrix n n 𝕜} (hQS : Q = S) : hQ.rpow r = ⋯.rpow r

theorem Matrix.PosDef.rpow_cast {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) {S : Matrix n n 𝕜} (hQS : Q = S) : hQ.rpow r = ⋯.rpow r

theorem Matrix.PosSemidef.rpow_cast {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) (r : ℝ) {S : Matrix n n 𝕜} (hQS : Q = S) : hQ.rpow r = ⋯.rpow r

theorem Matrix.posDefOne_rpow {𝕜 : Type u_2} [RCLike 𝕜] (n : Type u_1) [Fintype n] [DecidableEq n] (r : ℝ) : ⋯.rpow r = 1