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 pos_def.rpow as the matrix eigenvector_matrix * (coe ∘ diagonal (eigenvalues ^ r)) * eigenvector_matrix⁻¹.
It also proves some basic obvious properties of pos_def.rpow such as pos_def.rpow_mul_rpow and pos_def.rpow_zero.
noncomputable
def
matrix.pos_def.rpow
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def)
(r : ℝ) :
matrix n n 𝕜
Equations
- hQ.rpow r = ⇑(matrix.inner_aut ⟨_.eigenvector_matrix, _⟩) (coe ∘ matrix.diagonal (_.eigenvalues ^ r))
theorem
matrix.pos_def.rpow_one_eq_self
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def) :
theorem
matrix.pos_def.rpow_neg_one_eq_inv_self
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def) :
theorem
matrix.pos_def.rpow_zero
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def) :
theorem
matrix.pos_def.rpow.is_pos_def
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def)
(r : ℝ) :
theorem
matrix.pos_def.rpow.is_hermitian
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def)
(r : ℝ) :
(hQ.rpow r).is_hermitian
theorem
matrix.pos_def.inv
{𝕜 : Type u_1}
{n : Type u_2}
[fintype n]
[is_R_or_C 𝕜]
{Q : matrix n n 𝕜}
[decidable_eq 𝕜]
[decidable_eq n]
(hQ : Q.pos_def) :