Documentation

Monlib.LinearAlgebra.Matrix.PosDefRpow

The real-power of a positive definite matrix #

This file defines the real-power of a positive definite matrix. In particular, given a positive definite matrix x and real number r, we get posDef.rpow as the matrix eigenvector_matrix * (coe ∘ diagonal (eigenvalues ^ r)) * eigenvector_matrix⁻¹.

It also proves some basic obvious properties of posDef.rpow such as posDef.rpow_mul_rpow and posDef.rpow_zero.

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 𝕜

Equations

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

Instances For

@[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 𝕜

Equations

hQ.rpow r = ⋯.rpow r

Instances For

@[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 𝕜

Equations

hQ.rpow r = ⋯.rpow r

Instances For

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

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

theorem Matrix.PosSemidef.rpow_mul_rpow {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (r₁ : NNReal ˣ) (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

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 := ⋯ }

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) :

hQ.sqrt = 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) :

(⋯ : Q.PosSemidef).sqrt = 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 {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [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 {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [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 {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [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.IsHermitian.eigenvectorMatrix_conjTranspose_mul {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_1} [RCLike 𝕜] {x : Matrix n n 𝕜} (hx : x.IsHermitian) :

hx.eigenvectorMatrix.conjTranspose * hx.eigenvectorMatrix = 1

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

⋯.rpow r = 1