PhyslibSearch

theorem

The underlying matrix of a `HermitianMat` is self-adjoint

Let $A$ be a Hermitian matrix of type `HermitianMat n α`. Then its underlying matrix $A.\text{mat}$ is self-adjoint, meaning $A.\text{mat}^* = A.\text{mat}$ .

theorem

Any function is continuous on a finite subset of a $T_1$ space

#continuousOn_finite

Let $\alpha$ and $\beta$ be topological spaces, and let $S \subseteq \alpha$ be a finite subset of $\alpha$ . If $\alpha$ satisfies the $T_1$ separation axiom, then any function $f: \alpha \to \beta$ is continuous on $S$ .

theorem

The matrix $f(A)$ is self-adjoint for Hermitian $A$

#conjTranspose_cfc

Let $A$ be a Hermitian matrix of type `HermitianMat n α`, and let $A.\text{mat}$ denotes its underlying $n \times n$ matrix. Let $f$ be a function applied to the matrix via the Continuous Functional Calculus (CFC). Then the conjugate transpose of the resulting matrix is equal to itself, i.e., $(f(A.\text{mat}))^* = f(A.\text{mat})$ . In other words, applying the functional calculus to a Hermitian matrix results in a self-adjoint matrix.

definition

Continuous functional calculus for Hermitian matrices $\text{cfc}(f, A)$

#cfc

Let $d$ be a finite type and $\mathbb{k}$ be a field. For a Hermitian matrix $A \in \text{HermitianMat}_d(\mathbb{k})$ and a function $f: \mathbb{k} \to \mathbb{k}$ , $\text{cfc}(f, A)$ is the transformation of $A$ by applying the continuous functional calculus of $f$ to its underlying matrix representation $A_{\text{mat}}$ . The resulting matrix is also Hermitian.

theorem

The continuous functional calculus $A.\text{cfc } f$ equals the pair of $\text{cfc } f A.\text{mat}$ and its Hermitian proof

#cfc_eq

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜` and $f: \mathbb{R} \to \mathbb{R}$ be a function. The continuous functional calculus (CFC) of $A$ under $f$ , denoted as $A.\text{cfc } f$ , is equal to the Hermitian matrix formed by the pair consisting of the matrix-level continuous functional calculus $\text{cfc } f A.\text{mat}$ and the proof that this matrix satisfies the Hermitian property, denoted by $\text{cfc\_predicate } f A.\text{mat}$ .

theorem

The Underlying Matrix of the CFC for Hermitian Matrices is the CFC of the Underlying Matrix

#mat_cfc

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜` and $f: \mathbb{R} \to \mathbb{R}$ be a function. Then the underlying matrix of the continuous functional calculus (CFC) applied to $A$ using $f$ is equal to the continuous functional calculus applied to the underlying matrix of $A$ . That is, $(f(A))_{\text{mat}} = f(A_{\text{mat}})$ .

theorem

$A.\text{cfc}(f) = A.\text{cfc}(g)$ iff $f = g$ on $\sigma(A)$

#cfc_eq_cfc_iff_eqOn

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜` where $d$ is a finite index type and $\mathbb{k} = \mathbb{R}$ . For any two functions $f, g: \mathbb{R} \to \mathbb{R}$ , the results of the continuous functional calculus (CFC) applied to $A$ are equal, $A.\text{cfc}(f) = A.\text{cfc}(g)$ , if and only if $f$ and $g$ coincide on the spectrum of the underlying matrix $A.\text{mat}$ (denoted $\sigma(A)$ ).

theorem

$f|_{\sigma(A)} = g|_{\sigma(A)} \implies f(A) = g(A)$ for Hermitian matrices

#cfc_congr

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ where $d$ is a finite index type. For any two functions $f, g: \mathbb{R} \to \mathbb{R}$ , if $f$ and $g$ are equal on the spectrum of the underlying matrix $A_{\text{mat}}$ (denoted $\sigma(A)$ ), then applying the continuous functional calculus to $A$ with $f$ yields the same result as with $g$ , i.e., $f(A) = g(A)$ .

theorem

$f(A) = g(A)$ for $A \ge 0$ if $f, g$ agree on $[0, \infty)$

#cfc_congr_of_nonneg

Let $A$ be a Hermitian matrix such that $A \ge 0$ (i.e., $A$ is positive semidefinite). If two functions $f, g: \mathbb{R} \to \mathbb{R}$ agree on the interval $[0, \infty)$ (so that $f(x) = g(x)$ for all $x \ge 0$ ), then the continuous functional calculus (CFC) applied to $A$ yields the same result for both functions, i.e., $f(A) = g(A)$ .

theorem

$f|_{(0, \infty)} = g|_{(0, \infty)} \implies f(A) = g(A)$ for positive definite Hermitian matrices $A$ .

#cfc_congr_of_posDef

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ . If $A$ is positive definite (denoted by $A.\text{mat}.\text{PosDef}$ ) and two functions $f, g: \mathbb{R} \to \mathbb{R}$ agree on the set of positive real numbers $(0, \infty)$ , then the continuous functional calculus of $A$ applied to $f$ is equal to its application to $g$ , i.e., $f(A) = g(A)$ .

theorem

If $A$ and $B$ commute, then $f(A)$ and $B$ commute via CFC

#cfc_left

Let $A$ and $B$ be Hermitian matrices. If the underlying matrices of $A$ and $B$ commute (i.e., $A_{\text{mat}} B_{\text{mat}} = B_{\text{mat}} A_{\text{mat}}$ ), then for any function $f: \mathbb{R} \to \mathbb{R}$ , the matrix $(f(A))_{\text{mat}}$ obtained via continuous functional calculus also commutes with $B_{\text{mat}}$ .

theorem

$A$ commutes with $B \implies A$ commutes with $f(B)$ for Hermitian matrices

#cfc_right

Let $A$ and $B$ be Hermitian matrices. If the underlying matrix of $A$ commutes with the underlying matrix of $B$ (i.e., $A_{\text{mat}} B_{\text{mat}} = B_{\text{mat}} A_{\text{mat}}$ ), then for any function $f: \mathbb{R} \to \mathbb{R}$ , $A_{\text{mat}}$ also commutes with the matrix obtained by applying the continuous functional calculus of $f$ to $B$ , denoted $(B.\text{cfc } f)_{\text{mat}}$ .

theorem

If $A$ and $B$ commute, then $f(A)$ and $g(B)$ commute via CFC

#cfc_commute

Let $A$ and $B$ be Hermitian matrices. If the underlying matrices of $A$ and $B$ commute (i.e., $A.mat \cdot B.mat = B.mat \cdot A.mat$ ), then for any functions $f: \mathbb{R} \to \mathbb{R}$ and $g: \mathbb{R} \to \mathbb{R}$ , the matrices resulting from the continuous functional calculus (CFC), $(A.\text{cfc } f).mat$ and $(B.\text{cfc } g).mat$ , also commute.

theorem

CFC of a Hermitian Matrix commute with each other

#cfc_self_commute

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜`. For any two functions $f, g: \mathbb{R} \to \mathbb{R}$ , the matrices obtained by applying the continuous functional calculus (CFC) to $A$ commute with each other. That is, $(A.cfc(f)).mat \cdot (A.cfc(g)).mat = (A.cfc(g)).mat \cdot (A.cfc(f)).mat$ where $A.cfc(f)$ and $A.cfc(g)$ are the Hermitian matrices resulting from applying functions $f$ and $g$ to $A$ via the CFC, and $.mat$ denotes their underlying matrix representations.

theorem

CFC Commutes with Reindexing for Hermitian Matrices

#cfc_reindex

Let $A$ be a Hermitian matrix indexed by $d$ , and let $f: \mathbb{R} \to \mathbb{R}$ be a function. For any equivalence $e: d \simeq d_2$ between the index types $d$ and $d_2$ , the continuous functional calculus (CFC) of the reindexed Hermitian matrix satisfies: $(A.\text{reindex}(e)).\text{cfc}(f) = (A.\text{cfc}(f)).\text{reindex}(e)$ where $A.\text{reindex}(e)$ denotes the Hermitian matrix $A$ with both its rows and columns reindexed by $e$ , and $\text{cfc}$ denotes the application of the continuous functional calculus to the Hermitian matrix.

theorem

The spectrum of $f(A)$ is the image of the spectrum of $A$ under $f$ for Hermitian matrices

#spectrum_cfc_eq_image

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbf{k})$ and $f: \mathbb{R} \to \mathbb{R}$ be a function. Let $f(A)$ denote the matrix obtained by applying the continuous functional calculus to $A$ with respect to $f$ (denoted as `A.cfc f`). The spectrum of the matrix $f(A)$ is equal to the image of the spectrum of $A$ under the function $f$ , i.e., $\sigma(f(A)) = f(\sigma(A))$ .

theorem

Spectral decomposition of $(f(A))_{\text{mat}}$ as a sum of scaled projections

#cfc_toMat_eq_sum_smul_proj

Let $A$ be a Hermitian matrix and $f$ be a function. The underlying matrix of the continuous functional calculus $f(A)$ can be decomposed as the sum $(f(A))_{\text{mat}} = \sum_{i} f(\lambda_i) \cdot (U E_{ii} U^*)$ where $\lambda_i$ are the eigenvalues of $A$ , $U$ is the unitary matrix of eigenvectors (represented by `A.H.eigenvectorUnitary`), $E_{ii}$ is the elementary matrix with $1$ at position $(i, i)$ and $0$ elsewhere (represented by `Matrix.single i i 1`), and $U^*$ is the conjugate transpose of $U$ .

theorem

Eigenvalues of $f(A)$ for a Hermitian Matrix $A$ are $f$ applied to its Eigenvalues

#cfc_eigenvalues

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbf{k})$ , where $\mathbf{k}$ is a conjugate-reals-like field, and let $f: \mathbb{R} \to \mathbb{R}$ be a function. Let $f(A)$ denote the matrix obtained by applying the continuous functional calculus to $A$ with respect to $f$ (denoted in the formal statement as `A.cfc f`). Then there exists a permutation $\sigma: d \simeq d$ such that the eigenvalues of $f(A)$ are given by the composition $f \circ \lambda \circ \sigma$ , where $\lambda$ are the eigenvalues of $A$ . That is, the eigenvalues of the transformed matrix are the results of applying $f$ to the original eigenvalues, up to a reordering of the indices.

theorem

$A.\text{cfc}(\text{id}) = A$

#cfc_id

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜`. Let $\text{cfc}$ denote the continuous functional calculus for Hermitian matrices, and let $\text{id}$ be the identity function. Then applying the identity function to $A$ via the continuous functional calculus results in the matrix $A$ itself, i.e., $A.\text{cfc}(\text{id}) = A$ .

theorem

$A.\text{cfc}(\text{id}) = A$ for Hermitian matrices (identity map notation)

#cfc_id'

Let $A$ be a Hermitian matrix in $\text{HermitianMat}_d(\mathbb{k})$ and let $(\cdot)$ denote the identity function $x \mapsto x$ . Then, applying the continuous functional calculus to $A$ with respect to the identity function results in the matrix $A$ itself, i.e., $A.\text{cfc}(\cdot) = A$ .

theorem

$A.\text{cfc}(f + g) = A.\text{cfc}(f) + A.\text{cfc}(g)$ for Hermitian matrices

#cfc_add

Let $A$ be a Hermitian matrix in $\text{Herm}_d(\mathbb{k})$ . For any functions $f, g: \mathbb{k} \to \mathbb{k}$ , the continuous functional calculus (CFC) satisfies the additivity property: $A.\text{cfc}(f + g) = A.\text{cfc}(f) + A.\text{cfc}(g)$ where $f+g$ denotes the pointwise sum of the functions, and the addition on the right-hand side is the addition of Hermitian matrices.

theorem

$A.\text{cfc}(f+g) = A.\text{cfc}(f) + A.\text{cfc}(g)$ for Hermitian matrices via pointwise sum

#cfc_add_apply

Let $A$ be a Hermitian matrix in $\text{Herm}_d(\mathbb{k})$ and let $f$ and $g$ be functions from $\mathbb{k}$ to $\mathbb{k}$ . The continuous functional calculus applied to the pointwise sum $(f+g)(x) = f(x) + g(x)$ satisfies: $A.\text{cfc}(\lambda x. f(x) + g(x)) = A.\text{cfc}(f) + A.\text{cfc}(g)$ where the addition on the right-hand side is the addition of Hermitian matrices.

theorem

$A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)$ for Hermitian matrices

#cfc_sub

Let $A$ be a Hermitian matrix of size $d \times d$ over a field $\mathbb{k}$ . For any functions $f, g: \mathbb{k} \to \mathbb{k}$ , the continuous functional calculus (CFC) satisfies the following subtractivity property: $A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)$ where $f - g$ denotes the pointwise difference of the functions, and the subtraction on the right-hand side is the subtraction operation in the additive group of Hermitian matrices.

theorem

$A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)$ for Hermitian matrices

#cfc_sub_apply

Let $A$ be a Hermitian matrix of type $\text{HermitianMat}(n, \mathbb{k})$ . For any functions $f$ and $g$ in the domain of the continuous functional calculus for $A$ , the continuous functional calculus applied to their pointwise difference, $(f - g)(x) = f(x) - g(x)$ , is equal to the difference of the results of the functional calculus applied to $f$ and $g$ individually. That is, $A.\text{cfc}(\lambda x. f(x) - g(x)) = A.\text{cfc}(f) - A.\text{cfc}(g)$ .

theorem

$\text{cfc}(-f, A) = -\text{cfc}(f, A)$ for Hermitian matrices

#cfc_neg

Let $A$ be a Hermitian matrix of size $d \times d$ over a field $\mathbb{k}$ . For any function $f: \mathbb{k} \to \mathbb{k}$ , the continuous functional calculus (CFC) satisfies the following property: $\text{cfc}(-f, A) = -\text{cfc}(f, A)$ where $-f$ denotes the pointwise negation of the function, and the negation on the right-hand side is the additive inverse in the group of Hermitian matrices.

theorem

The continuous functional calculus of Hermitian matrices is odd with respect to the function argument ( $A.\text{cfc}(-f) = -A.\text{cfc}(f)$ ).

#cfc_neg_apply

Let $A$ be a Hermitian matrix in the type $\text{HermitianMat}(n, \alpha)$ . For any function $f$ in the domain of the continuous functional calculus for $A$ , the continuous functional calculus of the pointwise negation of $f$ , denoted by $x \mapsto -f(x)$ , is equal to the negation of the continuous functional calculus of $f$ in the additive group of Hermitian matrices. That is, $A.\text{cfc}(\lambda x. -f(x)) = -A.\text{cfc}(f)$ .

theorem

$(f \cdot g)(A) = f(A) \cdot g(A)$ for Hermitian matrices $A$ under Continuous Functional Calculus

#mat_cfc_mul

Let $A$ be a Hermitian matrix of type `HermitianMat n 𝕜`. For any functions $f, g: \mathbb{R} \to \mathbb{R}$ , the matrix representation of the continuous functional calculus (CFC) applied to the product $f \cdot g$ at $A$ is equal to the product of the matrix representations of the CFC of $f$ and $g$ at $A$ . That is, $(f \cdot g)(A) = f(A) \cdot g(A)$ .

theorem

The matrix of the functional calculus of a product is the product of the matrices: $(A.cfc (f \cdot g)).mat = A.cfc f \cdot A.cfc g$

#mat_cfc_mul_apply

Let $A$ be a Hermitian $n \times n$ matrix over $\mathbf{k}$ , where $\mathbf{k}$ is a field. For any continuous functions $f, g: \mathbb{R} \to \mathbb{R}$ (or appropriate scalar functions defined on the spectrum of $A$ ), the underlying matrix of the functional calculus of $A$ applied to the pointwise product of $f$ and $g$ is equal to the product of the matrices obtained by applying the functional calculus to $f$ and $g$ individually. That is, $(f \cdot g)(A) = f(A) \cdot g(A)$ where $(f \cdot g)(x) = f(x)g(x)$ .

theorem

$(g \circ f)(A) = g(f(A))$ for Continuous Functional Calculus on Hermitian Matrices

#cfc_comp

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜`. For any functions $f$ and $g$ such that the continuous functional calculus (CFC) is well-defined, the result of applying the composition $g \circ f$ to $A$ is equal to applying $g$ to the Hermitian matrix resulting from applying $f$ to $A$ . That is, $(g \circ f)(A) = g(f(A))$

theorem

Composition Law for Continuous Functional Calculus on Hermitian Matrices

#cfc_comp_apply

Let $A$ be a Hermitian matrix of type `HermitianMat d 𝕜`. For any functions $f$ and $g$ such that the continuous functional calculus (CFC) is well-defined, the matrix obtained by applying the composition $g \circ f$ to $A$ via the CFC is equal to the matrix obtained by first applying $f$ to $A$ and then applying $g$ to the resulting Hermitian matrix. That is, $A.\text{cfc}(x \mapsto g(f(x))) = (A.\text{cfc}(f)).\text{cfc}(g)$

theorem

$g(A) f(A) g(A)^\dagger = (f \cdot g^2)(A)$ for Hermitian matrices via CFC

#cfc_conj

Let $A$ be an $n \times n$ Hermitian matrix. For any real-valued functions $f$ and $g$ such that the continuous functional calculus (CFC) is well-defined, the congruence transformation of the matrix $f(A)$ by the matrix $g(A)$ satisfies: $g(A) f(A) g(A)^\dagger = (f \cdot g^2)(A)$ where $(\cdot)^\dagger$ denotes the conjugate transpose, and the right-hand side denotes the CFC applied to $A$ with the function $x \mapsto f(x)g(x)^2$ .

theorem

$\text{cfc}(f, \text{diag}(g)) = \text{diag}(f \circ g)$ for Hermitian matrices

#cfc_diagonal

Let $d$ be an index set and $\mathbb{k}$ be a field with a star-additive monoid structure (such as $\mathbb{R}$ or $\mathbb{C}$ ). Let $g: d \to \mathbb{R}$ be a function and let $\text{diag}(g)$ be the corresponding diagonal Hermitian matrix in $\text{HermitianMat}_d(\mathbb{k})$ . For a real-valued function $f: \mathbb{R} \to \mathbb{R}$ , the continuous functional calculus (CFC) of $f$ applied to the diagonal matrix is equal to the diagonal Hermitian matrix formed by the composition $f \circ g$ . That is, $\text{cfc}(f, \text{diag}(g)) = \text{diag}(f \circ g)$

theorem

CFC of Hermitian Matrices Commutes with Unitary Congruence

#cfc_conj_unitary

Let $A$ be a $d \times d$ Hermitian matrix over a field $\mathbb{k}$ and $U$ be a unitary matrix in the unitary group $U(d, \mathbb{k})$ . For any continuous function $f: \mathbb{R} \to \mathbb{R}$ , applying the continuous functional calculus (CFC) to the congruence transformation of $A$ by $U$ is equal to the congruence transformation of the CFC of $A$ by $U$ . That is, $f(U A U^\dagger) = U f(A) U^\dagger$ where $U^\dagger$ denotes the conjugate transpose of $U$ .

theorem

$f(A) = r \cdot I$ for constant functions $f(x) = r$ in the CFC of Hermitian matrices

#cfc_const

Let $A$ be a Hermitian matrix of size $d \times d$ over $\mathbb{k}$ , and let $r$ be a real constant. Let $f: \mathbb{R} \to \mathbb{R}$ be the constant function $f(x) = r$ . Then the continuous functional calculus (CFC) of $A$ with respect to $f$ , denoted $f(A)$ , is equal to the scalar multiple of the identity matrix by $r$ , i.e., $f(A) = r \cdot I$ .

theorem

The CFC of a Hermitian matrix $A$ for $f(x) = r \cdot x$ is $r \cdot A$

#cfc_const_mul_id

Let $A$ be a $d \times d$ Hermitian matrix over a field $\mathbb{k}$ , and let $r \in \mathbb{k}$ be a scalar. Let $f: \mathbb{k} \to \mathbb{k}$ be the function defined by $f(x) = r \cdot x$ . Then the continuous functional calculus (CFC) of $A$ with respect to $f$ is equal to the scalar multiplication of $r$ and $A$ , i.e., $f(A) = r \cdot A$ where $f(A)$ denotes the application of the functional calculus to $A$ with function $f$ .

theorem

The Continuous Functional Calculus for Hermitian matrices is $R$ -linear with respect to scalar multiplication.

#cfc_const_mul

Let $A$ be a Hermitian matrix of size $d \times d$ over a field $\mathbb{k}$ . For any scalar $r$ and any continuous function $f: \mathbb{k} \to \mathbb{k}$ , the Continuous Functional Calculus (CFC) applied to $A$ with the function $x \mapsto r \cdot f(x)$ is equal to the scalar multiple $r$ of the matrix obtained by applying the CFC to $A$ with the function $f$ . That is, $\text{cfc}(A, r \cdot f) = r \cdot \text{cfc}(A, f)$ where $\text{cfc}$ denotes the functional calculus for Hermitian matrices.

theorem

$\text{cfc}(0, f) = f(0) \cdot 1$ for Hermitian matrices

#cfc_apply_zero

Let $0$ be the zero Hermitian matrix of size $d \times d$ over the field $\mathbb{k}$ , and let $f: \mathbb{k} \to \mathbb{k}$ be a continuous function. The Continuous Functional Calculus (CFC) for Hermitian matrices applied to the zero matrix with the function $f$ is equal to the scalar $f(0)$ multiplied by the identity Hermitian matrix $1$ , i.e., $\text{cfc}(0, f) = f(0) \cdot 1$

theorem

$\text{cfc}(I, f) = f(1) \cdot I$ for Hermitian matrices

#cfc_apply_one

Let $I$ be the identity Hermitian matrix of type $\text{HermitianMat}_d(\mathbb{k})$ . For any continuous function $f: \mathbb{k} \to \mathbb{k}$ , the Continuous Functional Calculus (CFC) of $f$ applied to $I$ is equal to the scalar $f(1)$ times the identity matrix $I$ . That is, $\text{cfc}(I, f) = f(1) \cdot I$ where $1$ denotes the identity element in the algebra of Hermitian matrices.

theorem

$\text{cfc}(x \mapsto x^n, A) = A^n$ for Hermitian matrices

#cfc_pow

Let $A$ be a Hermitian matrix and $n$ be a natural number. Let $\text{cfc}$ denote the continuous functional calculus for Hermitian matrices. Then applying the power function $x \mapsto x^n$ to $A$ via the functional calculus yields the $n$ -th power of the matrix $A$ , i.e., $f(A) = A^n$ where $f(x) = x^n$ .

theorem

$0 \le f(A) \iff \forall i, 0 \le f(\lambda_i)$

#cfc_nonneg_iff

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ . For a function $f: \mathbb{R} \to \mathbb{R}$ , the matrix $f(A)$ (defined via the continuous functional calculus for Hermitian matrices) is positive semidefinite ( $0 \le f(A)$ ) if and only if $f(\lambda_i) \ge 0$ for all eigenvalues $\lambda_i$ of $A$ .

theorem

$f(A)$ is positive definite $\iff \forall i, f(\lambda_i) > 0$ for Hermitian matrices.

#cfc_posDef

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbf{k})$ and $f: \mathbb{R} \to \mathbb{R}$ be a function. The matrix $f(A)$ , obtained by applying the continuous functional calculus to $A$ with respect to $f$ , is positive definite if and only if $f(\lambda_i) > 0$ for all eigenvalues $\lambda_i$ of $A$ .

theorem

If $A \ge 0$ and $f \ge 0$ on the non-negative reals, then $f(A) \ge 0$ via CFC.

#cfc_nonneg_of_nonneg

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbb{k})$ and $f: \mathbb{R} \to \mathbb{R}$ be a real-valued function. If $A$ is positive semidefinite ( $0 \le A$ ) and $f(x) \ge 0$ for all $x \ge 0$ , then the matrix obtained by applying the continuous functional calculus (CFC) to $A$ via $f$ , denoted $f(A)$ , is also positive semidefinite ( $0 \le f(A)$ ).

theorem

$f(A)$ is non-singular if $f(\lambda_i) \neq 0$ for all eigenvalues $\lambda_i$ of $A$

#cfc_nonSingular

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbf{k})$ and $f: \mathbb{R} \to \mathbb{R}$ be a function. If for every eigenvalue $\lambda_i$ of $A$ , the value $f(\lambda_i)$ is non-zero, then the matrix $f(A)$ (obtained by applying the continuous functional calculus to $A$ with respect to $f$ ) is non-singular.

theorem

Trace of $A \cdot f(A)$ Equals $\sum \lambda_i f(\lambda_i)$

#trace_mul_cfc

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ and $f: \mathbb{R} \to \mathbb{R}$ be a real-valued function. Let $f(A)$ denote the matrix obtained by applying the continuous functional calculus to $A$ via $f$ . If $\lambda_i$ are the eigenvalues of $A$ , then the trace of the product of $A$ and $f(A)$ is given by the sum of the products of the eigenvalues and their images under $f$ : $\text{tr}(A \cdot f(A)) = \sum_{i} \lambda_i f(\lambda_i)$

theorem

The squared norm of a Hermitian matrix equals the sum of its squared eigenvalues $\|A\|^2 = \sum \lambda_i^2$

#norm_eq_sum_eigenvalues_sq

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbf{k})$ . The square of the Frobenius norm of $A$ , denoted $\|A\|^2$ , is equal to the sum of the squares of its eigenvalues $\lambda_i$ , i.e., $\|A\|^2 = \sum_{i \in d} \lambda_i^2$ .

theorem

If $\|A\| \le r$ , then $A \le r \cdot I$ for Hermitian matrices

#lt_smul_of_norm_lt

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ and let $r$ be a real number. If the norm of $A$ satisfies $\|A\| \le r$ , then $A$ is less than or equal to $r \cdot I$ in the Loewner partial order, where $I$ is the identity matrix.

theorem

$\text{Ball}(A, r) \subseteq [A - rI, A + rI]$ for Hermitian matrices

#ball_subset_Icc

For any Hermitian matrix $A \in \text{HermitianMat}_d(\mathbb{k})$ and any radius $r > 0$ , the open ball centered at $A$ with radius $r$ (with respect to the Frobenius norm) is a subset of the order interval $[A - rI, A + rI]$ defined by the Loewner partial order. That is, for any Hermitian matrix $B$ , if $\|B - A\| < r$ , then $A - rI \le B$ and $B \le A + rI$ , where $I$ is the identity matrix and the inequality $\le$ denotes that the difference is a positive semidefinite matrix.

theorem

If $A \le x \le B$ , then $\sigma(x)$ is contained in a bounded interval $[a, b]$ depending on $A$ and $B$ .

#spectrum_subset_of_mem_Icc

Let $d$ be a finite type and $\mathbb{k}$ be a real or complex field. For any two Hermitian matrices $A, B \in \text{HermitianMat}(d, \mathbb{k})$ , there exist real constants $a$ and $b$ such that for any Hermitian matrix $x$ , if $A \le x$ and $x \le B$ with respect to the Loewner partial order, then the real spectrum of the underlying matrix of $x$ , denoted $\sigma(x)$ , is contained within the closed interval $[a, b]$ .

theorem

The continuous functional calculus $A \mapsto f(A)$ is continuous on $\text{Herm}_d(\mathbb{C})$ for continuous $f$ .

#cfc_continuous

Let $d$ be a finite index set and $\mathbb{C}$ be the field of complex numbers. For any continuous function $f: \mathbb{R} \to \mathbb{R}$ , the map $A \mapsto f(A)$ from the space of Hermitian matrices $\text{Herm}_d(\mathbb{C})$ to itself, defined via the continuous functional calculus, is continuous.

theorem

The spectrum of a positive definite matrix is strictly positive ( $\sigma(A) \subseteq (0, \infty)$ )

#spectrum_subset_Ioi

Let $d$ be a finite type and $\mathbb{k}$ be a real or complex field (an `RCLike` field). For any $d \times d$ matrix $A$ over $\mathbb{k}$ , if $A$ is positive definite ( $A \succ 0$ ), then its spectrum $\sigma(A)$ is a subset of the open interval $(0, \infty)$ .

theorem

The map $x \mapsto A.\text{cfc}(f(x))$ is continuous if $f$ is a continuous family of functions.

#continuous_cfc_fun

Let $X$ be a topological space and $A$ be a Hermitian matrix of type $\text{HermitianMat}(d, \mathbb{k})$ . Let $f: X \to (\mathbb{R} \to \mathbb{R})$ be a family of functions such that for every $i \in \mathbb{R}$ , the map $x \mapsto f(x)(i)$ is continuous from $X$ to $\mathbb{R}$ . Then the map $x \mapsto A.\text{cfc}(f(x))$ , which applies the continuous functional calculus of $A$ to the function $f(x)$ , is a continuous map from $X$ to $\text{HermitianMat}(d, \mathbb{k})$ .

theorem

$x \mapsto f(x, A)$ is continuous on $S$ if $x \mapsto f(x, i)$ is continuous for $i \in \sigma(A)$

#continuousOn_cfc_fun

Let $A$ be an $n \times n$ Hermitian matrix over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$ ). Let $S$ and $T$ be sets of real numbers such that the spectrum of $A$ , denoted $\sigma(A)$ , is contained in $T$ . Let $f: S \times \mathbb{R} \to \mathbb{R}$ be a function such that for every $i \in T$ , the map $x \mapsto f(x, i)$ is continuous on $S$ . Then the map $x \mapsto f(x, A)$ (the continuous functional calculus of $A$ with respect to the parameter-dependent function $f$ ) is continuous on $S$ .

theorem

Upper bound on $\|f(A)\|$ by $\sqrt{|d|} \cdot \sup_{\sigma(A)} |f|$

#norm_cfc_le_sqrt_card_mul_bound

Let $d$ be a finite index set and $A \in \text{Herm}_d(\mathbb{C})$ be a complex Hermitian matrix. Let $f: \mathbb{R} \to \mathbb{R}$ be a function and $C \in \mathbb{R}$ be a non-negative constant. If $|f(x)| \leq C$ for all $x$ in the spectrum $\sigma(A)$ of the matrix $A$ , then the Frobenius norm of the matrix obtained by the continuous functional calculus $f(A)$ (denoted as `A.cfc f`) satisfies the inequality: $\|f(A)\| \leq \sqrt{|d|} \cdot C$ where $|d|$ denotes the cardinality of the index set $d$ .

theorem

$\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \sup_{\sigma(A)} |f - g|$ for Hermitian matrices

#norm_cfc_sub_cfc_le_sqrt_card

Let $d$ be a finite index set and $A$ be a complex Hermitian matrix of type $\text{HermitianMat}_d(\mathbb{C})$ . For any functions $f, g: \mathbb{R} \to \mathbb{R}$ , the Frobenius norm of the difference between the matrices obtained by the continuous functional calculus of $f$ and $g$ satisfies the inequality: $\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \sup_{x \in \sigma(A)} |f(x) - g(x)|$ where $|d|$ is the cardinality of the index set $d$ , and $\sigma(A)$ is the spectrum of the underlying matrix of $A$ .

theorem

$\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \epsilon$ if $\sup_T |f - g| \leq \epsilon$ and $\sigma(A) \subseteq T$

#norm_cfc_sub_le_of_sup_le

Let $d$ be a finite index set and $A \in \text{Herm}_d(\mathbb{C})$ be a complex Hermitian matrix. Let $f, g: \mathbb{R} \to \mathbb{R}$ be functions, $T \subseteq \mathbb{R}$ be a set, and $\epsilon \geq 0$ be a constant. If the spectrum of $A$ , denoted $\sigma(A)$ , is contained in $T$ ( $\sigma(A) \subseteq T$ ) and $|f(x) - g(x)| \leq \epsilon$ for all $x \in T$ , then the Frobenius norm of the difference between the matrices obtained by the continuous functional calculus, $f(A)$ and $g(A)$ , satisfies: $\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \epsilon$ where $|d|$ is the cardinality of the index set $d$ .

theorem

Uniform Continuity in $t$ for Jointly Continuous $f(x, t)$ on Compact $T$

#dist_lt_of_continuous'

Let $X$ be a topological space, $S \subseteq X$ be a set, and $T \subseteq \mathbb{R}$ be a compact set. Let $f: X \to (\mathbb{R} \to \mathbb{R})$ be a family of functions such that the joint map $(x, t) \mapsto f(x, t)$ is continuous on $S \times T$ . Then, for any $x_0 \in S$ and any $\epsilon > 0$ , there exists a neighborhood $U$ of $x_0$ such that for all $x \in U \cap S$ and all $t \in T$ , the inequality $\|f(x, t) - f(x_0, t)\| < \epsilon$ holds.

theorem

The functional calculus $A \mapsto g(A)$ is continuous on the set of Hermitian matrices with spectrum in a compact set $K$ for $g$ continuous on $K$

#continuousOn_cfc_of_compact

Let $d$ be a finite index set and $K \subseteq \mathbb{R}$ be a compact set. Let $g: \mathbb{R} \to \mathbb{R}$ be a function that is continuous on $K$ . Then the map $A \mapsto g(A)$ , defined by the continuous functional calculus for Hermitian matrices, is continuous on the set of complex Hermitian matrices $\text{Herm}_d(\mathbb{C})$ whose spectrum is contained in $K$ .

theorem

Joint Continuity of Continuous Functional Calculus $x \mapsto f(x)(A(x))$ on Compact Domains

#continuous_cfc_joint_compact

Let $X$ be a topological space and $d$ be a finite index set. Let $S \subseteq X$ and $T \subseteq \mathbb{R}$ be sets, where $T$ is compact. Suppose we have a family of functions mapping into the real numbers $f : X \to (\mathbb{R} \to \mathbb{R})$ and a family of complex Hermitian matrices $A : X \to \text{Herm}_d(\mathbb{C})$ . If: 1. The joint map $(x, t) \mapsto f(x, t)$ is continuous on $S \times T$ , 2. For all $x \in S$ , the spectrum of the underlying matrix of $A(x)$ is contained in $T$ (i.e., $\sigma(A(x)) \subseteq T$ ), and 3. The map $x \mapsto A(x)$ is continuous on $S$ with respect to the matrix norm, then the map $x \mapsto f(x)(A(x))$ , defined via the continuous functional calculus for Hermitian matrices, is continuous on $S$ .

theorem

Eigenvalues of a complex Hermitian matrix are bounded by the matrix norm $| \lambda_i | \leq \|A\|$

#eigenvalue_norm_le

Let $A$ be a complex Hermitian matrix of dimension $d$ , and let $\lambda_i$ denote its $i$ -th eigenvalue for $i \in d$ . The absolute value of any eigenvalue is bounded by the Frobenius norm of the matrix, i.e., $|\lambda_i| \leq \|A\|$ .

theorem

Spectrum of a Hermitian Matrix is Contained in the Closed Ball of Radius $\|A\|$

#spectrum_subset_closedBall

Let $A$ be a complex Hermitian matrix of dimension $d$ . The spectrum of its underlying matrix, denoted $\sigma_{\mathbb{R}}(A)$ , is contained in the closed ball in $\mathbb{R}$ centered at $0$ with radius equal to the norm of $A$ . That is, $\sigma_{\mathbb{R}}(A) \subseteq \{x \in \mathbb{R} : |x| \le \|A\|\}$ .

theorem

The Property of the Spectrum being Contained in an Open Set is Stable under Small Perturbations of Hermitian Matrices

#spectrum_subset_of_isOpen

Let $A_0$ be a $d \times d$ complex Hermitian matrix and let $U \subseteq \mathbb{R}$ be an open set. If the spectrum of $A_0$ is contained in $U$ , then for all Hermitian matrices $B$ in a sufficiently small neighborhood of $A_0$ , the spectrum of $B$ is also contained in $U$ .

theorem

Continuity of the Hermitian functional calculus $B \mapsto g(B)$ at $A_0$ for $g$ continuous on $T \supseteq \sigma(A_0)$

#continuousWithinAt_cfc_of_continuousOn

Let $d$ be a finite index set and $\text{Herm}_d(\mathbb{C})$ be the space of $d \times d$ complex Hermitian matrices. Let $g: \mathbb{R} \to \mathbb{R}$ be a function and $T \subseteq \mathbb{R}$ be a set such that $g$ is continuous on $T$ . If $A_0 \in \text{Herm}_d(\mathbb{C})$ is a Hermitian matrix whose spectrum $\sigma(A_0)$ is contained in $T$ , then the continuous functional calculus map $B \mapsto g(B)$ is continuous at $A_0$ when restricted to the set of Hermitian matrices $B$ whose spectra $\sigma(B)$ are also contained in $T$ .

theorem

Uniform bound on $f$ over the spectrum of a continuous family of Hermitian matrices $A$ .

#dist_lt_of_continuous_spectrum

Let $X$ be a topological space, $d$ an index type, and $\text{HermitianMat}(d, \mathbb{C})$ the space of $d \times d$ complex Hermitian matrices. Let $f: X \times \mathbb{R} \to \mathbb{R}$ be a function and $A: X \to \text{HermitianMat}(d, \mathbb{C})$ be a family of Hermitian matrices. Suppose $S \subseteq X$ and $T \subseteq \mathbb{R}$ are sets such that: 1. The function $(x, t) \mapsto f(x, t)$ is continuous on the product set $S \times T$ . 2. For every $x \in S$ , the spectrum of the matrix $A(x)$ is contained in $T$ . 3. The map $x \mapsto A(x)$ is continuous on $S$ . Then for any $x_0 \in S$ and any $\epsilon > 0$ , there exists a neighborhood $U$ of $x_0$ such that for all $y \in U \cap S$ and every eigenvalue $t$ in the spectrum of $A(y)$ , the inequality $\|f(y, t) - f(x_0, t)\| < \epsilon$ holds.

theorem

Joint Continuity of Continuous Functional Calculus for Hermitian Matrices

#continuous_cfc_joint

Let $X$ be a topological space and $d$ be a finite index set. Let $f: X \to (\mathbb{R} \to \mathbb{R})$ be a family of functions and $A: X \to \text{HermitianMat}_d(\mathbb{C})$ be a family of complex Hermitian matrices. Suppose $S \subseteq X$ and $T \subseteq \mathbb{R}$ are sets such that: 1. The map $(x, t) \mapsto f(x, t)$ is continuous on $S \times T$ . 2. For every $x \in S$ , the spectrum of the matrix $A(x)$ is contained in $T$ . 3. The map $x \mapsto A(x)$ is continuous on $S$ . Then the mapping $x \mapsto (A(x)).\text{cfc}(f(x))$ is continuous on $S$ , where $\text{cfc}$ denotes the continuous functional calculus for Hermitian matrices.

theorem

The map $x \mapsto f(x, A)$ is continuous on $S$ for nonsingular $A$ if $x \mapsto f(x, i)$ is continuous for $i \neq 0$

#continuousOn_cfc_fun_nonsingular

Let $X$ be a topological space and $A$ be a nonsingular Hermitian matrix of size $d \times d$ over $\mathbb{C}$ . Let $f: X \times \mathbb{R} \to \mathbb{R}$ be a function and $S \subseteq X$ be a set. If for every non-zero real number $i \neq 0$ , the map $x \mapsto f(x, i)$ is continuous on $S$ , then the map $x \mapsto f(x, A)$ (defined via the continuous functional calculus for Hermitian matrices) is also continuous on $S$ .

theorem

Continuity of $f(x, A)$ for positive semidefinite $A$ and $f$ continuous on $[0, \infty)$

#continuousOn_cfc_fun_nonneg

Let $X$ be a topological space and $S \subseteq X$ be a subset. Let $A$ be a Hermitian matrix such that $0 \le A$ (i.e., $A$ is positive semidefinite). Let $f: X \times \mathbb{R} \to \mathbb{R}$ be a function such that for every $i \ge 0$ , the map $x \mapsto f(x, i)$ is continuous on $S$ . Then the map $x \mapsto f(x, A)$ , defined via the continuous functional calculus for Hermitian matrices, is continuous on $S$ .

theorem

The map $x \mapsto f(x, A)$ is continuous on $S$ for positive definite $A$ if $f(x, \cdot)$ is continuous on $(0, \infty)$

#continuousOn_cfc_fun_posDef

Let $A$ be a Hermitian matrix such that its underlying matrix $A_{\text{mat}}$ is positive definite ( $A \succ 0$ ). Let $f: X \times \mathbb{R} \to \mathbb{R}$ be a function and $S$ be a subset of a topological space $X$ . If for every $i \in (0, \infty)$ , the function $x \mapsto f(x, i)$ is continuous on $S$ , then the map $x \mapsto f(x, A)$ defined via the continuous functional calculus is continuous on $S$ with respect to the topology on the space of Hermitian matrices.

theorem

$(f(A))^{-1} = f^{-1}(A)$ for Hermitian matrices

#inv_cfc_eq_cfc_inv

Let $A$ be a Hermitian matrix and $f$ be a function such that for every eigenvalue $\lambda_i$ of $A$ , $f(\lambda_i) \neq 0$ . Then the inverse of the matrix obtained by the continuous functional calculus (CFC) of $f$ on $A$ is equal to the matrix obtained by the CFC of the inverse function $u \mapsto f(u)^{-1}$ on $A$ . That is, $(f(A))^{-1} = f^{-1}(A)$ .

theorem

The continuous functional calculus of $u \mapsto u^{-1}$ for a non-singular Hermitian matrix $A$ equals $A^{-1}$

#cfc_inv

Let $A$ be a non-singular Hermitian matrix indexed by $d$ with entries in $\mathbb{k}$ . Then the continuous functional calculus of $A$ applied to the inversion function $u \mapsto u^{-1}$ is equal to the matrix inverse $A^{-1}$ . Here, $A^{-1}$ denotes the inverse in the space of Hermitian matrices.

theorem

The integral of a Hermitian matrix function commutes with its matrix representation.

#integral_toMat

Let $A: \mathbb{R} \to \text{Herm}_d(\mathbb{k})$ be a function mapping real numbers to the space of $d \times d$ Hermitian matrices over $\mathbb{k}$ , and let $\mu$ be a measure on $\mathbb{R}$ . For any $T_1, T_2 \in \mathbb{R}$ , if $A$ is interval integrable with respect to $\mu$ over the interval from $T_1$ to $T_2$ , then the underlying matrix of the integral of $A$ is equal to the integral of the underlying matrix function of $A$ . That is, $\left( \int_{T_1}^{T_2} A(t) \, \partial \mu \right)_{\text{mat}} = \int_{T_1}^{T_2} (A(t))_{\text{mat}} \, \partial \mu$ where $(\cdot)_{\text{mat}}$ denotes the map from a Hermitian matrix to its representation as a $d \times d$ matrix.

theorem

Interval integrability of a sum of scaled constant matrices

#intervalIntegrable_sum_smul_const

Let $T_1, T_2 \in \mathbb{R}$ be two real numbers and $\mu$ be a measure on $\mathbb{R}$ . Let $g: \mathbb{R} \to (d \to \mathbb{R})$ be a collection of scalar functions $g_i(t)$ indexed by $i \in d$ , and let $P_i$ be a collection of matrices. If for every index $i$ , the scalar function $t \mapsto g_i(t)$ is interval integrable with respect to $\mu$ over $[T_1, T_2]$ , then the sum of scaled constant matrices $t \mapsto \sum_{i} g_i(t) \cdot P_i$ is also interval integrable over the same interval.

theorem

A function to Hermitian matrices is interval integrable iff its matrix values are interval integrable

#intervalIntegrable_toMat_iff

Let $d$ be a finite index set and $\mathbb{k}$ be a field (such as $\mathbb{R}$ or $\mathbb{C}$ ). Let $A: \mathbb{R} \to \text{Herm}_d(\mathbb{k})$ be a function mapping real numbers to Hermitian matrices, and let $T_1, T_2 \in \mathbb{R}$ be endpoints of an interval with respect to a measure $\mu$ on $\mathbb{R}$ . Then the function $t \mapsto (A(t))_{\text{mat}}$ , which maps $t$ to the underlying $d \times d$ matrix of $A(t)$ , is interval integrable if and only if the function $A$ is interval integrable as a map into the space of Hermitian matrices.

theorem

The continuous functional calculus $f_t(A)$ is interval integrable if $f_t(\lambda_i)$ is interval integrable for all eigenvalues $\lambda_i$

#integrable_cfc

Let $A$ be a Hermitian matrix with eigenvalues $\lambda_i$ . Let $f: \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ be a family of functions indexed by $t \in \mathbb{R}$ , denoted $f_t(x)$ . For a given interval $[T_1, T_2]$ and a measure $\mu$ on $\mathbb{R}$ , if for every eigenvalue $\lambda_i$ of $A$ , the scalar function $t \mapsto f_t(\lambda_i)$ is interval integrable over $[T_1, T_2]$ , then the function $t \mapsto f_t(A)$ (the continuous functional calculus of $A$ with respect to $f_t$ ) is interval integrable over $[T_1, T_2]$ in the space of Hermitian matrices.

theorem

$\int f(t, A) \, dt = (\int f(t, \cdot) \, dt)(A)$ for Hermitian matrices

#integral_cfc_eq_cfc_integral

Let $A$ be a Hermitian matrix of type $\text{HermitianMat}(d, \mathbb{k})$ and let $\lambda_i$ denote its eigenvalues. Let $f: \mathbb{R} \to \mathbb{R} \to \mathbb{R}$ be a function such that for each eigenvalue $\lambda_i$ , the function $t \mapsto f(t, \lambda_i)$ is interval integrable with respect to a measure $\mu$ on the interval $[T_1, T_2]$ . Then the integral of the continuous functional calculus (CFC) of $A$ with respect to $f(t, \cdot)$ is equal to the continuous functional calculus of $A$ applied to the integral of $f$ , 즉: $\int_{T_1}^{T_2} f(t, A) \, d\mu(t) = \left( \int_{T_1}^{T_2} f(t, \cdot) \, d\mu(t) \right)(A)$ where $f(t, A)$ denotes the application of the functional calculus to $A$ using the function $f$ at a fixed $t$ .

theorem

$0 < A \implies 0 < f(A)$ for positive $f$ on $(0, \infty)$ and non-negative $f(0)$

#cfc_pos_of_pos

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ and $f: \mathbb{R} \to \mathbb{R}$ be a function. If $A$ is positive definite ( $0 < A$ ), and $f$ satisfies $f(i) > 0$ for all $i > 0$ and $f(0) \ge 0$ , then the matrix obtained via the functional calculus $f(A)$ is also positive definite ( $0 < f(A)$ ).

theorem

Commuting Hermitian matrices have a common preimage in the Continuous Functional Calculus

#exists_HermitianMat_cfc

Let $A$ and $B$ be Hermitian matrices of type $\text{HermitianMat}(d, \mathbb{k})$ . If their underlying matrices $A.\text{mat}$ and $B.\text{mat}$ commute, then there exists a common Hermitian matrix $C \in \text{HermitianMat}(d, \mathbb{k})$ and functions $f, g: \mathbb{R} \to \mathbb{R}$ such that $A$ is the functional calculus of $C$ by $f$ ( $A = f(C)$ ) and $B$ is the functional calculus of $C$ by $g$ ( $B = g(C)$ ).

theorem

$f \le g$ on $(0, \infty)$ implies $A.\text{cfc}(f) \le A.\text{cfc}(g)$ for positive definite $A$

#cfc_le_cfc_of_PosDef

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ such that its underlying matrix $A.\text{mat}$ is positive definite ( $A.\text{mat} > 0$ ). Let $f, g: \mathbb{R} \to \mathbb{R}$ be functions such that for all $i > 0$ , $f(i) \le g(i)$ . Then, the matrix obtained by applying the continuous functional calculus of $f$ to $A$ is less than or equal to the matrix obtained by applying the continuous functional calculus of $g$ to $A$ with respect to the Loewner partial order, i.e., $A.\text{cfc}(f) \le A.\text{cfc}(g)$ .

theorem

Monotonicity of $\text{cfc}$ on Positive Definite Matrices for Commuting $A \le B$

#cfc_le_cfc_of_commute_monoOn

Let $A$ and $B$ be $d \times d$ Hermitian matrices over $\mathbb{k}$ such that their underlying matrices $A.\text{mat}$ and $B.\text{mat}$ commute. Suppose that both $A$ and $B$ are positive definite ( $A.\text{mat}.PosDef$ and $B.\text{mat}.PosDef$ ) and that $A \le B$ with respect to the Loewner partial order. If $f: \mathbb{R} \to \mathbb{R}$ is a function that is monotone on the interval $(0, \infty)$ , then the matrices obtained by the continuous functional calculus satisfy $A.\text{cfc} f \le B.\text{cfc} f$ .

theorem

$A \le B$ and $\text{Commute}(A, B) \implies f(A) \le f(B)$ for monotone $f$

#cfc_le_cfc_of_commute

Let $A$ and $B$ be Hermitian matrices of type $\text{HermitianMat}(d, \mathbb{k})$ such that their underlying matrices $A.\text{mat}$ and $B.\text{mat}$ commute. If $A \le B$ with respect to the Loewner partial order and $f: \mathbb{R} \to \mathbb{R}$ is a monotone function, then the matrices obtained via the continuous functional calculus satisfy $f(A) \le f(B)$ .

theorem

$\text{False} \implies$ Monotonicity of $f(A)$ on positive definite Hermitian matrices

#cfc_monoOn_pos_of_monoOn_posDef

Let $d$ be a finite index set and $f: \mathbb{R} \to \mathbb{R}$ be a function. Assuming a contradiction (the proposition $\text{False}$ ), the continuous functional calculus $A \mapsto f(A)$ is monotone on the set of positive definite Hermitian matrices $A \in \text{HermitianMat}_d(\mathbb{C})$ with respect to the Loewner partial order. Specifically, for any two positive definite Hermitian matrices $A$ and $B$ , if $A \le B$ in the Loewner order, then $f(A) \le f(B)$ .

theorem

$A \le I \implies I \le A^{-1}$ for positive definite Hermitian matrices

#inv_ge_one_of_le_one

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(d, \mathbb{k})$ . If $A$ is positive definite ( $A > 0$ ) and $A$ is less than or equal to the identity matrix ( $A \le I$ ) in the Loewner partial order, then the matrix inverse $A^{-1}$ is greater than or equal to the identity matrix ( $I \le A^{-1}$ ).

theorem

$\text{trace}(f(A)) = \sum f(\lambda_i)$ for Hermitian matrices

#trace_cfc_eq

Let $A$ be a Hermitian matrix of dimension $d$ over $\mathbb{C}$ . For any continuous function $f: \mathbb{R} \to \mathbb{R}$ , the trace of the matrix obtained by applying the continuous functional calculus to $A$ with respect to $f$ , denoted as $\text{trace}(f(A))$ , is equal to the sum of the function $f$ applied to each eigenvalue $\lambda_i$ of $A$ : $\text{trace}(f(A)) = \sum_{i \in d} f(\lambda_i)$ where $\lambda_i$ are the eigenvalues of $A$ provided by the spectral theorem for Hermitian matrices.

theorem

$Ax = 0$ iff $x$ is Orthogonal to Eigenvectors of Non-zero Eigenvalues of $A$

#mulVec_eq_zero_iff_inner_eigenvector_zero

Let $A$ be a $d \times d$ Hermitian matrix over $\mathbb{C}$ and let $x \in \mathbb{C}^d$ be a vector in the corresponding Euclidean space. Let $\lambda_i$ denote the eigenvalues and $v_i$ denote the corresponding orthonormal eigenvector basis of $A$ . Then $Ax = 0$ if and only if for all indices $i$ such that $\lambda_i \neq 0$ , the inner product of $v_i$ and $x$ is zero, i.e., $\langle v_i, x \rangle = 0$ .

theorem

Eigenvector expansion of $f(A)x$ for Hermitian matrices

#cfc_mulVec_expansion

Let $A$ be a Hermitian matrix of dimension $d$ over $\mathbb{C}$ , and let $f: \mathbb{R} \to \mathbb{R}$ be a function. For any vector $x$ in the Euclidean space $\mathbb{C}^d$ , the result of the matrix-vector multiplication of $f(A)$ and $x$ can be expanded in terms of the eigenvectors of $A$ as: $(f(A))x = \sum_{i} f(\lambda_i) \langle v_i, x \rangle v_i$ where $\lambda_i$ are the eigenvalues and $v_i$ are the corresponding orthonormal eigenvectors of $A$ (as provided by the spectral decomposition `A.H`), and $\langle \cdot, \cdot \rangle$ denotes the inner product on $\mathbb{C}^d$ .

theorem

$\ker(f(A)) \subseteq \ker(A)$ if $f(\lambda)=0 \implies \lambda=0$ on the spectrum of $A$ .

#ker_cfc_le_ker_on_set

Let $A$ be a Hermitian matrix of size $d \times d$ over $\mathbb{C}$ . Let $s \subseteq \mathbb{R}$ be a set containing the spectrum of $A$ , and let $f: \mathbb{R} \to \mathbb{R}$ be a function. If for all $\lambda \in s$ , $f(\lambda) = 0$ implies $\lambda = 0$ , then the kernel of the matrix obtained by the continuous functional calculus $f(A)$ is a subspace of the kernel of $A$ , i.e., $\ker(f(A)) \subseteq \ker(A)$ .

theorem

$(f(i) = 0 \to i = 0) \implies \ker(f(A)) \le \ker(A)$

#ker_cfc_le_ker

Let $A$ be a Hermitian matrix and $f: \mathbb{R} \to \mathbb{R}$ be a function. If $f$ satisfies the property that for any $i \in \mathbb{R}$ , $f(i) = 0$ implies $i = 0$ , then the kernel of the matrix $f(A)$ (obtained via the continuous functional calculus) is a submodule of the kernel of $A$ , denoted as $\ker(f(A)) \le \ker(A)$ .

theorem

$\ker(f(A)) \le \ker A$ for positive semidefinite $A$ if $f(i)=0 \implies i=0$ for $i \ge 0$

#ker_cfc_le_ker_nonneg

Let $A$ be a Hermitian matrix such that $A$ is positive semidefinite ( $0 \le A$ in the Loewner order). Let $f: \mathbb{R} \to \mathbb{R}$ be a function such that for all $i \ge 0$ , if $f(i) = 0$ then $i = 0$ . Then the kernel of the matrix obtained by the continuous functional calculus, $\ker(f(A))$ , is a submodule of the kernel of $A$ , i.e., $\ker(f(A)) \le \ker A$ .

theorem

$\sigma(A) \subseteq s \text{ and } (i \in s, i=0 \implies f(i)=0) \implies \ker(A) \le \ker(f(A))$

#ker_le_ker_cfc_on_set

Let $A$ be a Hermitian matrix of size $d \times d$ over $\mathbb{C}$ . Let $s \subseteq \mathbb{R}$ be a set containing the spectrum of $A$ , i.e., $\sigma(A) \subseteq s$ . Let $f: \mathbb{R} \to \mathbb{R}$ be a function such that for all $i \in s$ , if $i = 0$ then $f(i) = 0$ . Then the kernel of $A$ is a submodule of the kernel of the matrix obtained by applying the continuous functional calculus to $A$ with respect to $f$ , denoted as $\ker(A) \le \ker(f(A))$ .

theorem

$f(0) = 0 \implies \ker A \subseteq \ker f(A)$ for a Hermitian matrix $A$

#ker_le_ker_cfc

Let $A$ be a Hermitian matrix and $f$ be a continuous function. If $f(0) = 0$ , then the kernel of $A$ is a subspace of the kernel of the matrix obtained by applying the continuous functional calculus to $A$ with $f$ , denoted by $f(A)$ . That is, $\ker A \subseteq \ker f(A)$ .

theorem

$\ker A \le \ker(f(A))$ for positive semidefinite $A$ and functions vanishing at zero

#ker_le_ker_cfc_nonneg

Let $A$ be a Hermitian matrix such that $A \ge 0$ (i.e., $A$ is positive semidefinite). Let $f$ be a function such that for all $i \ge 0$ , if $i = 0$ then $f(i) = 0$ . Then the kernel of $A$ is a subspace of the kernel of the matrix obtained by applying the continuous functional calculus to $A$ with respect to $f$ , denoted $\ker A \le \ker(f(A))$ .

theorem

$\ker(f(A)) = \ker A$ if $f(i) = 0 \iff i = 0$

#ker_cfc_eq_ker

Let $A$ be a Hermitian $n \times n$ matrix over a field $\mathbb{k}$ and $f: \mathbb{k} \to \mathbb{k}$ be a function. If for all $i \in \mathbb{k}$ , $f(i) = 0$ if and only if $i = 0$ , then the kernel of the matrix obtained by the continuous functional calculus $\ker(f(A))$ is equal to the kernel of the original matrix $\ker A$ .

theorem

$\ker(f(A)) = \ker A$ for non-negative $A$ and $f(i)=0 \leftrightarrow i=0$

#ker_cfc_eq_ker_nonneg

Let $A$ be a Hermitian matrix such that $0 \le A$ (i.e., $A$ is positive semidefinite). Let $f$ be a function such that for all $i \ge 0$ , $f(i) = 0$ if and only if $i = 0$ . Then the kernel of the matrix obtained by the continuous functional calculus $\ker(f(A))$ is equal to the kernel of $A$ , denoted $\ker A$ .

QuantumInfo.ForMathlib.HermitianMat.CFC

The underlying matrix of a `HermitianMat` is self-adjoint

Any function is continuous on a finite subset of a T1T_1T1​ space

The matrix f(A)f(A)f(A) is self-adjoint for Hermitian AAA

Continuous functional calculus for Hermitian matrices cfc(f,A) \text{cfc}(f, A) cfc(f,A)

The continuous functional calculus A.cfc fA.\text{cfc } fA.cfc f equals the pair of cfc fA.mat\text{cfc } f A.\text{mat}cfc fA.mat and its Hermitian proof

The Underlying Matrix of the CFC for Hermitian Matrices is the CFC of the Underlying Matrix

A.cfc(f)=A.cfc(g)A.\text{cfc}(f) = A.\text{cfc}(g)A.cfc(f)=A.cfc(g) iff f=gf = gf=g on σ(A)\sigma(A)σ(A)

f∣σ(A)=g∣σ(A) ⟹ f(A)=g(A)f|_{\sigma(A)} = g|_{\sigma(A)} \implies f(A) = g(A)f∣σ(A)​=g∣σ(A)​⟹f(A)=g(A) for Hermitian matrices

f(A)=g(A)f(A) = g(A)f(A)=g(A) for A≥0A \ge 0A≥0 if f,gf, gf,g agree on [0,∞)[0, \infty)[0,∞)

f∣(0,∞)=g∣(0,∞) ⟹ f(A)=g(A)f|_{(0, \infty)} = g|_{(0, \infty)} \implies f(A) = g(A)f∣(0,∞)​=g∣(0,∞)​⟹f(A)=g(A) for positive definite Hermitian matrices AAA.

If AAA and BBB commute, then f(A)f(A)f(A) and BBB commute via CFC

AAA commutes with B ⟹ AB \implies AB⟹A commutes with f(B)f(B)f(B) for Hermitian matrices

If AAA and BBB commute, then f(A)f(A)f(A) and g(B)g(B)g(B) commute via CFC

CFC of a Hermitian Matrix commute with each other

CFC Commutes with Reindexing for Hermitian Matrices

The spectrum of f(A)f(A)f(A) is the image of the spectrum of AAA under fff for Hermitian matrices

Spectral decomposition of (f(A))mat(f(A))_{\text{mat}}(f(A))mat​ as a sum of scaled projections

Eigenvalues of f(A)f(A)f(A) for a Hermitian Matrix AAA are fff applied to its Eigenvalues

A.cfc(id)=AA.\text{cfc}(\text{id}) = AA.cfc(id)=A

A.cfc(id)=AA.\text{cfc}(\text{id}) = AA.cfc(id)=A for Hermitian matrices (identity map notation)

A.cfc(f+g)=A.cfc(f)+A.cfc(g)A.\text{cfc}(f + g) = A.\text{cfc}(f) + A.\text{cfc}(g)A.cfc(f+g)=A.cfc(f)+A.cfc(g) for Hermitian matrices

A.cfc(f+g)=A.cfc(f)+A.cfc(g)A.\text{cfc}(f+g) = A.\text{cfc}(f) + A.\text{cfc}(g)A.cfc(f+g)=A.cfc(f)+A.cfc(g) for Hermitian matrices via pointwise sum

A.cfc(f−g)=A.cfc(f)−A.cfc(g)A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)A.cfc(f−g)=A.cfc(f)−A.cfc(g) for Hermitian matrices

A.cfc(f−g)=A.cfc(f)−A.cfc(g)A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)A.cfc(f−g)=A.cfc(f)−A.cfc(g) for Hermitian matrices

cfc(−f,A)=−cfc(f,A)\text{cfc}(-f, A) = -\text{cfc}(f, A)cfc(−f,A)=−cfc(f,A) for Hermitian matrices

The continuous functional calculus of Hermitian matrices is odd with respect to the function argument (A.cfc(−f)=−A.cfc(f)A.\text{cfc}(-f) = -A.\text{cfc}(f)A.cfc(−f)=−A.cfc(f)).

(f⋅g)(A)=f(A)⋅g(A)(f \cdot g)(A) = f(A) \cdot g(A)(f⋅g)(A)=f(A)⋅g(A) for Hermitian matrices AAA under Continuous Functional Calculus

The matrix of the functional calculus of a product is the product of the matrices: (A.cfc(f⋅g)).mat=A.cfcf⋅A.cfcg(A.cfc (f \cdot g)).mat = A.cfc f \cdot A.cfc g(A.cfc(f⋅g)).mat=A.cfcf⋅A.cfcg

(g∘f)(A)=g(f(A))(g \circ f)(A) = g(f(A))(g∘f)(A)=g(f(A)) for Continuous Functional Calculus on Hermitian Matrices

Composition Law for Continuous Functional Calculus on Hermitian Matrices

g(A)f(A)g(A)†=(f⋅g2)(A)g(A) f(A) g(A)^\dagger = (f \cdot g^2)(A)g(A)f(A)g(A)†=(f⋅g2)(A) for Hermitian matrices via CFC

cfc(f,diag(g))=diag(f∘g)\text{cfc}(f, \text{diag}(g)) = \text{diag}(f \circ g)cfc(f,diag(g))=diag(f∘g) for Hermitian matrices

CFC of Hermitian Matrices Commutes with Unitary Congruence

f(A)=r⋅If(A) = r \cdot If(A)=r⋅I for constant functions f(x)=rf(x) = rf(x)=r in the CFC of Hermitian matrices

The CFC of a Hermitian matrix AAA for f(x)=r⋅xf(x) = r \cdot xf(x)=r⋅x is r⋅Ar \cdot Ar⋅A

The Continuous Functional Calculus for Hermitian matrices is RRR-linear with respect to scalar multiplication.

cfc(0,f)=f(0)⋅1\text{cfc}(0, f) = f(0) \cdot 1cfc(0,f)=f(0)⋅1 for Hermitian matrices

cfc(I,f)=f(1)⋅I\text{cfc}(I, f) = f(1) \cdot Icfc(I,f)=f(1)⋅I for Hermitian matrices

cfc(x↦xn,A)=An\text{cfc}(x \mapsto x^n, A) = A^ncfc(x↦xn,A)=An for Hermitian matrices

0≤f(A) ⟺ ∀i,0≤f(λi)0 \le f(A) \iff \forall i, 0 \le f(\lambda_i)0≤f(A)⟺∀i,0≤f(λi​)

f(A)f(A)f(A) is positive definite ⟺ ∀i,f(λi)>0\iff \forall i, f(\lambda_i) > 0⟺∀i,f(λi​)>0 for Hermitian matrices.

If A≥0A \ge 0A≥0 and f≥0f \ge 0f≥0 on the non-negative reals, then f(A)≥0f(A) \ge 0f(A)≥0 via CFC.

f(A)f(A)f(A) is non-singular if f(λi)≠0f(\lambda_i) \neq 0f(λi​)=0 for all eigenvalues λi\lambda_iλi​ of AAA

Trace of A⋅f(A)A \cdot f(A)A⋅f(A) Equals ∑λif(λi)\sum \lambda_i f(\lambda_i)∑λi​f(λi​)

The squared norm of a Hermitian matrix equals the sum of its squared eigenvalues ∥A∥2=∑λi2\|A\|^2 = \sum \lambda_i^2∥A∥2=∑λi2​

If ∥A∥≤r\|A\| \le r∥A∥≤r, then A≤r⋅IA \le r \cdot IA≤r⋅I for Hermitian matrices

Ball(A,r)⊆[A−rI,A+rI]\text{Ball}(A, r) \subseteq [A - rI, A + rI]Ball(A,r)⊆[A−rI,A+rI] for Hermitian matrices

If A≤x≤BA \le x \le BA≤x≤B, then σ(x)\sigma(x)σ(x) is contained in a bounded interval [a,b][a, b][a,b] depending on AAA and BBB.

The continuous functional calculus A↦f(A)A \mapsto f(A)A↦f(A) is continuous on Hermd(C)\text{Herm}_d(\mathbb{C})Hermd​(C) for continuous fff.

The spectrum of a positive definite matrix is strictly positive (σ(A)⊆(0,∞)\sigma(A) \subseteq (0, \infty)σ(A)⊆(0,∞))

The map x↦A.cfc(f(x))x \mapsto A.\text{cfc}(f(x))x↦A.cfc(f(x)) is continuous if fff is a continuous family of functions.

x↦f(x,A)x \mapsto f(x, A)x↦f(x,A) is continuous on SSS if x↦f(x,i)x \mapsto f(x, i)x↦f(x,i) is continuous for i∈σ(A)i \in \sigma(A)i∈σ(A)

Upper bound on ∥f(A)∥\|f(A)\|∥f(A)∥ by ∣d∣⋅sup⁡σ(A)∣f∣\sqrt{|d|} \cdot \sup_{\sigma(A)} |f|∣d∣​⋅supσ(A)​∣f∣

∥f(A)−g(A)∥≤∣d∣⋅sup⁡σ(A)∣f−g∣\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \sup_{\sigma(A)} |f - g|∥f(A)−g(A)∥≤∣d∣​⋅supσ(A)​∣f−g∣ for Hermitian matrices

∥f(A)−g(A)∥≤∣d∣⋅ϵ\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \epsilon∥f(A)−g(A)∥≤∣d∣​⋅ϵ if sup⁡T∣f−g∣≤ϵ\sup_T |f - g| \leq \epsilonsupT​∣f−g∣≤ϵ and σ(A)⊆T\sigma(A) \subseteq Tσ(A)⊆T

Uniform Continuity in ttt for Jointly Continuous f(x,t)f(x, t)f(x,t) on Compact TTT

The functional calculus A↦g(A)A \mapsto g(A)A↦g(A) is continuous on the set of Hermitian matrices with spectrum in a compact set KKK for ggg continuous on KKK

Joint Continuity of Continuous Functional Calculus x↦f(x)(A(x))x \mapsto f(x)(A(x))x↦f(x)(A(x)) on Compact Domains

Eigenvalues of a complex Hermitian matrix are bounded by the matrix norm ∣λi∣≤∥A∥| \lambda_i | \leq \|A\|∣λi​∣≤∥A∥

Spectrum of a Hermitian Matrix is Contained in the Closed Ball of Radius ∥A∥\|A\|∥A∥

The Property of the Spectrum being Contained in an Open Set is Stable under Small Perturbations of Hermitian Matrices

Continuity of the Hermitian functional calculus B↦g(B)B \mapsto g(B)B↦g(B) at A0A_0A0​ for ggg continuous on T⊇σ(A0)T \supseteq \sigma(A_0)T⊇σ(A0​)

Uniform bound on fff over the spectrum of a continuous family of Hermitian matrices AAA.

Joint Continuity of Continuous Functional Calculus for Hermitian Matrices

The map x↦f(x,A)x \mapsto f(x, A)x↦f(x,A) is continuous on SSS for nonsingular AAA if x↦f(x,i)x \mapsto f(x, i)x↦f(x,i) is continuous for i≠0i \neq 0i=0

Continuity of f(x,A)f(x, A)f(x,A) for positive semidefinite AAA and fff continuous on [0,∞)[0, \infty)[0,∞)

The map x↦f(x,A)x \mapsto f(x, A)x↦f(x,A) is continuous on SSS for positive definite AAA if f(x,⋅)f(x, \cdot)f(x,⋅) is continuous on (0,∞)(0, \infty)(0,∞)

(f(A))−1=f−1(A)(f(A))^{-1} = f^{-1}(A)(f(A))−1=f−1(A) for Hermitian matrices

The continuous functional calculus of u↦u−1u \mapsto u^{-1}u↦u−1 for a non-singular Hermitian matrix AAA equals A−1A^{-1}A−1

The integral of a Hermitian matrix function commutes with its matrix representation.

Interval integrability of a sum of scaled constant matrices

A function to Hermitian matrices is interval integrable iff its matrix values are interval integrable

The continuous functional calculus ft(A)f_t(A)ft​(A) is interval integrable if ft(λi)f_t(\lambda_i)ft​(λi​) is interval integrable for all eigenvalues λi\lambda_iλi​

∫f(t,A) dt=(∫f(t,⋅) dt)(A)\int f(t, A) \, dt = (\int f(t, \cdot) \, dt)(A)∫f(t,A)dt=(∫f(t,⋅)dt)(A) for Hermitian matrices

0<A ⟹ 0<f(A)0 < A \implies 0 < f(A)0<A⟹0<f(A) for positive fff on (0,∞)(0, \infty)(0,∞) and non-negative f(0)f(0)f(0)

Commuting Hermitian matrices have a common preimage in the Continuous Functional Calculus

f≤gf \le gf≤g on (0,∞)(0, \infty)(0,∞) implies A.cfc(f)≤A.cfc(g)A.\text{cfc}(f) \le A.\text{cfc}(g)A.cfc(f)≤A.cfc(g) for positive definite AAA

Monotonicity of cfc\text{cfc}cfc on Positive Definite Matrices for Commuting A≤BA \le BA≤B

A≤BA \le BA≤B and Commute(A,B) ⟹ f(A)≤f(B)\text{Commute}(A, B) \implies f(A) \le f(B)Commute(A,B)⟹f(A)≤f(B) for monotone fff

Any function is continuous on a finite subset of a $T_1$ space

The matrix $f(A)$ is self-adjoint for Hermitian $A$

Continuous functional calculus for Hermitian matrices $\text{cfc}(f, A)$

The continuous functional calculus $A.\text{cfc } f$ equals the pair of $\text{cfc } f A.\text{mat}$ and its Hermitian proof

$A.\text{cfc}(f) = A.\text{cfc}(g)$ iff $f = g$ on $\sigma(A)$

$f|_{\sigma(A)} = g|_{\sigma(A)} \implies f(A) = g(A)$ for Hermitian matrices

$f(A) = g(A)$ for $A \ge 0$ if $f, g$ agree on $[0, \infty)$

$f|_{(0, \infty)} = g|_{(0, \infty)} \implies f(A) = g(A)$ for positive definite Hermitian matrices $A$ .

If $A$ and $B$ commute, then $f(A)$ and $B$ commute via CFC

$A$ commutes with $B \implies A$ commutes with $f(B)$ for Hermitian matrices

If $A$ and $B$ commute, then $f(A)$ and $g(B)$ commute via CFC

The spectrum of $f(A)$ is the image of the spectrum of $A$ under $f$ for Hermitian matrices

Spectral decomposition of $(f(A))_{\text{mat}}$ as a sum of scaled projections

Eigenvalues of $f(A)$ for a Hermitian Matrix $A$ are $f$ applied to its Eigenvalues

$A.\text{cfc}(\text{id}) = A$

$A.\text{cfc}(\text{id}) = A$ for Hermitian matrices (identity map notation)

$A.\text{cfc}(f + g) = A.\text{cfc}(f) + A.\text{cfc}(g)$ for Hermitian matrices

$A.\text{cfc}(f+g) = A.\text{cfc}(f) + A.\text{cfc}(g)$ for Hermitian matrices via pointwise sum

$A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)$ for Hermitian matrices

$A.\text{cfc}(f - g) = A.\text{cfc}(f) - A.\text{cfc}(g)$ for Hermitian matrices

$\text{cfc}(-f, A) = -\text{cfc}(f, A)$ for Hermitian matrices

The continuous functional calculus of Hermitian matrices is odd with respect to the function argument ( $A.\text{cfc}(-f) = -A.\text{cfc}(f)$ ).

$(f \cdot g)(A) = f(A) \cdot g(A)$ for Hermitian matrices $A$ under Continuous Functional Calculus

The matrix of the functional calculus of a product is the product of the matrices: $(A.cfc (f \cdot g)).mat = A.cfc f \cdot A.cfc g$

$(g \circ f)(A) = g(f(A))$ for Continuous Functional Calculus on Hermitian Matrices

$g(A) f(A) g(A)^\dagger = (f \cdot g^2)(A)$ for Hermitian matrices via CFC

$\text{cfc}(f, \text{diag}(g)) = \text{diag}(f \circ g)$ for Hermitian matrices

$f(A) = r \cdot I$ for constant functions $f(x) = r$ in the CFC of Hermitian matrices

The CFC of a Hermitian matrix $A$ for $f(x) = r \cdot x$ is $r \cdot A$

The Continuous Functional Calculus for Hermitian matrices is $R$ -linear with respect to scalar multiplication.

$\text{cfc}(0, f) = f(0) \cdot 1$ for Hermitian matrices

$\text{cfc}(I, f) = f(1) \cdot I$ for Hermitian matrices

$\text{cfc}(x \mapsto x^n, A) = A^n$ for Hermitian matrices

$0 \le f(A) \iff \forall i, 0 \le f(\lambda_i)$

$f(A)$ is positive definite $\iff \forall i, f(\lambda_i) > 0$ for Hermitian matrices.

If $A \ge 0$ and $f \ge 0$ on the non-negative reals, then $f(A) \ge 0$ via CFC.

$f(A)$ is non-singular if $f(\lambda_i) \neq 0$ for all eigenvalues $\lambda_i$ of $A$

Trace of $A \cdot f(A)$ Equals $\sum \lambda_i f(\lambda_i)$

The squared norm of a Hermitian matrix equals the sum of its squared eigenvalues $\|A\|^2 = \sum \lambda_i^2$

If $\|A\| \le r$ , then $A \le r \cdot I$ for Hermitian matrices

$\text{Ball}(A, r) \subseteq [A - rI, A + rI]$ for Hermitian matrices

If $A \le x \le B$ , then $\sigma(x)$ is contained in a bounded interval $[a, b]$ depending on $A$ and $B$ .

The continuous functional calculus $A \mapsto f(A)$ is continuous on $\text{Herm}_d(\mathbb{C})$ for continuous $f$ .

The spectrum of a positive definite matrix is strictly positive ( $\sigma(A) \subseteq (0, \infty)$ )

The map $x \mapsto A.\text{cfc}(f(x))$ is continuous if $f$ is a continuous family of functions.

$x \mapsto f(x, A)$ is continuous on $S$ if $x \mapsto f(x, i)$ is continuous for $i \in \sigma(A)$

Upper bound on $\|f(A)\|$ by $\sqrt{|d|} \cdot \sup_{\sigma(A)} |f|$

$\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \sup_{\sigma(A)} |f - g|$ for Hermitian matrices

$\|f(A) - g(A)\| \leq \sqrt{|d|} \cdot \epsilon$ if $\sup_T |f - g| \leq \epsilon$ and $\sigma(A) \subseteq T$

Uniform Continuity in $t$ for Jointly Continuous $f(x, t)$ on Compact $T$

The functional calculus $A \mapsto g(A)$ is continuous on the set of Hermitian matrices with spectrum in a compact set $K$ for $g$ continuous on $K$

Joint Continuity of Continuous Functional Calculus $x \mapsto f(x)(A(x))$ on Compact Domains

Eigenvalues of a complex Hermitian matrix are bounded by the matrix norm $| \lambda_i | \leq \|A\|$

Spectrum of a Hermitian Matrix is Contained in the Closed Ball of Radius $\|A\|$

Continuity of the Hermitian functional calculus $B \mapsto g(B)$ at $A_0$ for $g$ continuous on $T \supseteq \sigma(A_0)$

Uniform bound on $f$ over the spectrum of a continuous family of Hermitian matrices $A$ .

The map $x \mapsto f(x, A)$ is continuous on $S$ for nonsingular $A$ if $x \mapsto f(x, i)$ is continuous for $i \neq 0$

Continuity of $f(x, A)$ for positive semidefinite $A$ and $f$ continuous on $[0, \infty)$

The map $x \mapsto f(x, A)$ is continuous on $S$ for positive definite $A$ if $f(x, \cdot)$ is continuous on $(0, \infty)$

$(f(A))^{-1} = f^{-1}(A)$ for Hermitian matrices

The continuous functional calculus of $u \mapsto u^{-1}$ for a non-singular Hermitian matrix $A$ equals $A^{-1}$

The continuous functional calculus $f_t(A)$ is interval integrable if $f_t(\lambda_i)$ is interval integrable for all eigenvalues $\lambda_i$

$\int f(t, A) \, dt = (\int f(t, \cdot) \, dt)(A)$ for Hermitian matrices

$0 < A \implies 0 < f(A)$ for positive $f$ on $(0, \infty)$ and non-negative $f(0)$

$f \le g$ on $(0, \infty)$ implies $A.\text{cfc}(f) \le A.\text{cfc}(g)$ for positive definite $A$

Monotonicity of $\text{cfc}$ on Positive Definite Matrices for Commuting $A \le B$

$A \le B$ and $\text{Commute}(A, B) \implies f(A) \le f(B)$ for monotone $f$

$\text{False} \implies$ Monotonicity of $f(A)$ on positive definite Hermitian matrices

$A \le I \implies I \le A^{-1}$ for positive definite Hermitian matrices

$\text{trace}(f(A)) = \sum f(\lambda_i)$ for Hermitian matrices

$Ax = 0$ iff $x$ is Orthogonal to Eigenvectors of Non-zero Eigenvalues of $A$

Eigenvector expansion of $f(A)x$ for Hermitian matrices

$\ker(f(A)) \subseteq \ker(A)$ if $f(\lambda)=0 \implies \lambda=0$ on the spectrum of $A$ .

$(f(i) = 0 \to i = 0) \implies \ker(f(A)) \le \ker(A)$

$\ker(f(A)) \le \ker A$ for positive semidefinite $A$ if $f(i)=0 \implies i=0$ for $i \ge 0$

$\sigma(A) \subseteq s \text{ and } (i \in s, i=0 \implies f(i)=0) \implies \ker(A) \le \ker(f(A))$

$f(0) = 0 \implies \ker A \subseteq \ker f(A)$ for a Hermitian matrix $A$

$\ker A \le \ker(f(A))$ for positive semidefinite $A$ and functions vanishing at zero

$\ker(f(A)) = \ker A$ if $f(i) = 0 \iff i = 0$

$\ker(f(A)) = \ker A$ for non-negative $A$ and $f(i)=0 \leftrightarrow i=0$