QuantumInfo.ForMathlib.HermitianMat.Sqrt

Given a Hermitian matrix $A \in \text{HermitianMat}_d(\mathbb{k})$, its square root $A^{1/2}$ is defined using the continuous functional calculus (CFC). Specifically, $A^{1/2} = f(A)$ where $f(x) = \sqrt{x}$ for $x \geq 0$ and $f(x) = 0$ for $x < 0$. The resulting matrix is also a Hermitian matrix of the same dimension.

For any Hermitian matrix $A \in \text{HermitianMat}_d(\mathbb{k})$, the product of its square root matrix with itself is equal to its positive-semidefinite part, denoted $A^+$. That is, $A.\text{sqrt}.\text{mat} \cdot A.\text{sqrt}.\text{mat} = A^+$.

Let $A$ be a Hermitian matrix. If $A$ is positive semi-definite (denoted by $0 \le A$), then the square of its square root matrix is equal to $A$, i.e., $A^{1/2} A^{1/2} = A$.

Let $A$ and $B$ be Hermitian matrices. If the matrix $A$ commutes with the matrix $B$, then the square root of $A$ (denoted $A^{1/2}$) also commutes with $B$. In other terms, if $AB = BA$, then $A^{1/2}B = BA^{1/2}$.

Let $A$ and $B$ be Hermitian matrices of dimension $d$ over the field $\mathbb{k}$. If $A$ commutes with $B$ (i.e., $AB = BA$), then $A$ also commutes with the square root of $B$, denoted by $\sqrt{B}$. That is, $A \sqrt{B} = \sqrt{B} A$.

Let $A$ be a Hermitian matrix in $\mathbb{k}^{d \times d}$. If $A$ is a positive definite matrix, then $A^{-1/2} A A^{-1/2} = I$, where $A^{-1/2}$ denotes the square root of the inverse of $A$ and $I$ is the identity matrix.

For any Hermitian matrix $A$ of dimension $d$ over the field $\mathbb{k}$, its square root $\sqrt{A}$ is a non-negative operator, denoted by $0 \le \sqrt{A}$.

Let $A$ be a Hermitian matrix of dimension $d$ over the field $\mathbb{k}$. If $A$ is strictly positive-definite (denoted $0 < A$), then its square root $A^{1/2}$ (denoted `A.sqrt`) is also strictly positive-definite ($0 < A^{1/2}$).

Let $A$ be a Hermitian matrix of dimension $d$ over the field $\mathbb{k}$. If the underlying matrix of $A$ (denoted $A.\text{mat}$) is positive-definite, then the underlying matrix of the square root of $A$ (denoted $A^{1/2}.\text{mat}$) is also positive-definite.

This is a tactic extension for the `positivity` framework that automatically proves the positivity or nonnegativity of the square root of a Hermitian matrix. Given an expression of the form $A^{1/2}$ (denoted `HermitianMat.sqrt A`), the extension attempts to determine if $A$ is strictly positive-definite ($A > 0$). If $A > 0$ is established, it returns a proof that $A^{1/2} > 0$ using the theorem `HermitianMat.sqrt_pos`. Otherwise, it falls back to providing a proof of nonnegativity ($A^{1/2} \ge 0$) using the theorem `HermitianMat.sqrt_nonneg`.