QuantumInfo.ForMathlib.HermitianMat.Rpow
50 declarations
Real power of a Hermitian matrix via functional calculus
#rpowGiven a Hermitian matrix and a real number , the matrix power is defined via the continuous functional calculus (CFC). Specifically, if is diagonalized as , then , where the power function is applied elementwise to the diagonal entries of using the real power function . Note that if an eigenvalue is and , the result follows the convention .
Real exponentiation for Hermitian matrices
#instRPowFor a finite-dimensional Hilbert space , let denote the set of Hermitian matrices over the field . This definition provides an instance of the real power operator \text{^} : \text{Herm}_d(\mathbb{k}) \times \mathbb{R} \to \text{Herm}_d(\mathbb{k}). For a Hermitian matrix and a real exponent , is defined via the functional calculus (specifically `HermitianMat.rpow`), such that if has spectral decomposition , then .
Real Power Commutes with Unitary Conjugation of Hermitian Matrices
#rpow_conj_unitaryLet be a Hermitian matrix of dimension over the field , and let be a unitary matrix (an element of the unitary group ). For any real exponent , the -th power of the conjugated matrix is equal to the conjugation of the -th power of by . That is, .
For a Hermitian matrix and a real number , the power operation is equivalent to the matrix power function `rpow` applied to and .
Let be a Hermitian matrix and be a real number. Then the matrix power is equal to the result of applying the continuous functional calculus to with the real power function .
for Hermitian matrices
#diagonal_powLet be a function and be the diagonal matrix whose entries are given by for . For any real exponent , the -th power of the diagonal matrix is the diagonal matrix of the -th powers of its entries, i.e., .
The map is continuous on Hermitian matrices for
#rpow_const_continuousLet be the space of complex matrices, and let denote the subspace of Hermitian matrices. For any real number , the function that maps a Hermitian matrix to its matrix power , defined via the continuous functional calculus, is continuous.
The function is continuous for non-singular
#const_rpow_continuousLet be a non-singular Hermitian matrix in . Then the map is continuous for all , where denotes the matrix power with real exponent.
The map is continuous for for Hermitian
#continuousOn_rpow_posLet be a Hermitian matrix in . Then the map is continuous on the interval , where denotes the matrix power of with real exponent .
The map is continuous for
#continuousOn_rpow_negLet be a Hermitian matrix in . The function , which maps a real number to the -th power of the matrix , is continuous on the interval .
for Hermitian matrices
#rpow_oneFor any Hermitian matrix , raising to the power of the real number results in the matrix itself, i.e., .
for Hermitian matrices
#sqrt_eq_cfc_rpow_halfFor any Hermitian matrix , the square root of (defined via the continuous functional calculus of ) is equal to the continuous functional calculus of the function applied to .
for Hermitian matrices
#one_rpowLet denote the identity matrix in the space of Hermitian matrices of dimension over the field . For any real number , the -th power of the identity matrix is equal to the identity matrix. That is, where the power is defined via the continuous functional calculus for Hermitian matrices.
for Hermitian Matrices
#rpow_zeroFor any Hermitian matrix , the real power of with exponent is the identity matrix . That is, where denotes the identity matrix of the same dimension as .
Real Power of a Diagonal Matrix equals the Diagonal Matrix of Real Powers
#rpow_diagonalLet be a finite index set and be a function representing the diagonal entries of a square matrix. For any real exponent , the -th power of the diagonal matrix with entries is equal to the diagonal matrix whose entries are the -th powers of the original entries. That is, where the -th diagonal entry of the resulting matrix is .
Real power commutes with matrix reindexing ( reindexed equals reindexed )
#reindex_rpowLet be a Hermitian matrix indexed by , and let be a bijection between index sets. For any real exponent , the -th power of the matrix reindexed by is equal to the reindexing of the -th power of . That is, where the reindexing operation permutes the rows and columns of the matrix according to the equivalence .
Exponent Addition Law for Real Powers of Semidefinite Hermitian Matrices ()
#mat_rpow_addLet be a semidefinite Hermitian matrix (). For any real numbers and satisfying , the -th power of is equal to the product of the -th power of and the -th power of . That is, provided that the sum of the exponents is non-zero.
for Positive Semidefinite Hermitian Matrices
#rpow_mulLet be a Hermitian matrix such that (i.e., is positive semidefinite). For any real numbers and , the matrix powers satisfy the identity . Here, denotes the power of a Hermitian matrix with a real exponent .
Conjugation of Matrix Powers for Hermitian
#conj_rpowLet be a positive semidefinite Hermitian matrix (). For any real numbers and such that and , the conjugation of by , defined as , is equal to .
for
#pow_half_mulLet be a positive semi-definite Hermitian matrix (denoted ). Then the product of the matrix power with itself is equal to , i.e., .
Real powers of positive definite matrices are positive definite
#rpow_posLet be a Hermitian matrix in (or ). If is positive definite (denoted ), then for any real power , the matrix power is also positive definite, namely .
Real powers of positive semi-definite matrices are positive semi-definite
#rpow_nonnegLet be a Hermitian matrix such that (i.e., is positive semi-definite). Then for any real power , the matrix power is also positive semi-definite, denoted as .
for positive definite Hermitian matrices
#inv_eq_rpow_neg_oneLet be a Hermitian matrix. If is positive definite (denoted as ), then its inverse matrix is equal to its real power with exponent , namely .
Conjugation of by equals
#sandwich_selfLet be a positive definite Hermitian matrix. Then the conjugation of by the matrix results in the identity matrix, i.e., .
for Positive Definite Hermitian Matrices
#rpow_inv_eq_neg_rpowLet be a Hermitian matrix in and let be a real number. If is positive definite (), then the inverse of the -th power of is equal to raised to the power of , i.e., .
for positive definite
#sandwich_le_oneLet and be Hermitian matrices of dimension over a field . If is a positive definite matrix and in the Loewner order (meaning is positive semidefinite), then the "sandwich" operation of by satisfies where is the identity matrix and denotes the real power of the Hermitian matrix with exponent .
for Positive Definite Hermitian Matrix
#rpow_neg_mul_rpow_selfLet be a Hermitian matrix and assume that is positive definite. For any real number , the product of the matrix raised to the power and the matrix raised to the power is the identity matrix, i.e., .
is Invertible for Positive Definite
#isUnit_rpow_toMatLet be a Hermitian matrix and be a real number. If is positive definite, then the matrix power is an invertible matrix.
Inverse of Sandwiched by equals Sandwiched by
#sandwich_invLet and be Hermitian matrices. Suppose is positive definite. Then the inverse of the congruence transformation of by is equal to the congruence transformation of by . That is, where denotes the conjugate transpose and is the sandwich (congruence) operator.
For and ,
#ker_rpow_eq_of_nonnegLet be a Hermitian matrix over the complex numbers . If is positive semi-definite (i.e., ) and is a non-zero real number, then the kernel of the matrix power is equal to the kernel of . In symbols, .
For ,
#ker_rpow_le_of_nonnegLet be a Hermitian matrix of dimension over the complex numbers . If is positive semi-definite (i.e., ), then the kernel of the matrix power is a subspace of the kernel of , denoted as .
Congruence Transformation Distributes over Kronecker Product
#conj_kronLet be a matrix and be a matrix over a field . Let and be Hermitian matrices of dimensions and respectively. Then the congruence transformation of the Kronecker product by the Kronecker product is equal to the Kronecker product of the individual congruence transformations. That is, where denotes the congruence transformation of by , and denotes the Kronecker product.
Real Power of Kronecker Product is the Kronecker Product of Real Powers
#rpow_kronLet and be complex Hermitian matrices of dimensions and respectively. If and are positive semi-definite (i.e., and in the Loewner order), then for any real number , the -th power of their Kronecker product is equal to the Kronecker product of their individual -th powers. That is, where denotes the Kronecker product and denotes the matrix power with a real exponent.
Continuity of in the uniform topology on compact sets
#continuousOn_rpow_uniformLet be a compact set. Let be the set of positive real numbers. The function that maps an exponent to the power function is continuous on with respect to the topology of uniform convergence on . Specifically, the map is continuous from the subset of the real numbers to the space of functions on endowed with the uniform norm.
Joint Continuity of Hermitian Matrix Power for
#continuousOn_rpow_joint_nonneg_posLet be a topological space and a subset. Suppose is a continuous mapping from into the space of complex Hermitian matrices, and is a continuous real-valued function on . If for all , then the mapping is continuous on , where denotes the matrix power defined via the continuous functional calculus.
for Positive Semidefinite Hermitian Matrices
#cfc_sq_rpow_eq_cfc_rpowLet be a Hermitian matrix of dimension over the complex numbers , and assume that is positive semidefinite (). For any real number , the continuous functional calculus of applied to the function is equal to the continuous functional calculus of applied to the function . That is, .
for Hermitian matrices
#trace_rpow_eq_sumFor any complex Hermitian matrix of dimension and any real number , the trace of the -th power of is equal to the sum of the -th powers of its eigenvalues. Specifically, if denotes the -th eigenvalue of for , then
Finite integral approximation for matrix power
#rpowApproxFor a complex Hermitian matrix and real numbers , we define the finite integral approximation: where denotes the identity matrix. This expression serves as a truncated integral representation used to prove the operator monotonicity of the power function .
The approximation is operator monotone for and
#rpowApprox_monoLet and be complex Hermitian matrices. Suppose and are positive definite (denoted and ). If in the Loewner order (meaning is positive semidefinite), then for any real number and any real parameter , the approximating operators satisfy .
Scalar function for the approximation of real matrix powers
#scalarRpowApproxGiven real numbers , , and , this function is defined as the integral: This function serves as the scalar basis for the approximation of the real power of a Hermitian matrix via the Continuous Functional Calculus (CFC).
Approximated Hermitian matrix power equals functional calculus of on
#rpowApprox_eq_cfc_scalarLet be a positive definite Hermitian matrix of dimension over . For any real numbers and such that and , the approximated matrix power (denoted by `rpowApprox A q T`) is equal to the result of applying the scalar function (denoted by `scalarRpowApprox q T`) to the matrix via the continuous functional calculus.
The integral
#rpowConstFor a real number , the function returns the value of the integral as a real number. This constant appears in the integral representation of the power function and is equal to for .
Integrability of on for
#rpowConst_integrableOnLet be a real number such that . Then the function is integrable on the interval .
for
#rpowConst_posLet be a real number such that . Then the constant (defined as `rpowConst q`) is strictly positive.
Pointwise convergence of to as
#scalarRpowApprox_tendstoFor any real numbers , such that , , the scalar function converges to as , where denotes the constant .
converges to as
#tendsto_rpowApproxLet be a positive definite Hermitian matrix of dimension over . For any real number such that , the matrix-valued function converges to as in the topology of the normed space of Hermitian matrices, where denotes the constant and is the identity matrix.
Loewner-Heinz inequality for positive definite matrices: for
#rpow_le_rpow_of_posDefLet and be complex Hermitian matrices of dimension . If is positive definite (), is less than or equal to in the Loewner order (), and is a real number such that , then .
Löwner—Heinz Theorem:
#rpow_le_rpow_of_leLet and be complex Hermitian matrices of dimension . If and , then , where the inequalities denote the Loewner partial order.
Let and be positive semi-definite complex Hermitian matrices (i.e., and ). For any real number such that , the following inequality of Lieb-Thirring type holds for the trace: Here, denotes the -th power of a Hermitian matrix , and for a Hermitian matrix and matrix , represents the congruent transformation . In the case where or , the trace terms correspond to and respectively.
Trace of is Subadditive for
#trace_rpow_add_leLet and be complex Hermitian matrices of dimension . If and are positive semi-definite (i.e., and ) and is a real number such that , then the trace of the sum raised to the power is less than or equal to the sum of the traces of the individual matrices raised to the same power:
