Linear functionals #
This file contains results for linear functionals on the set of $n \times n$ matrices $M_n$ over $\mathbb{C}$.
Main results #
module.dual.applymodule.dual.is_pos_map_iffmodule.dual.is_faithful_pos_map_iffmodule.dual.is_tracial_faithful_pos_map_iffmodule.dual.is_faithful_pos_map_iff_is_inner
the matrix of a linear map φ : M_n →ₗ[R] R is given by
∑ i j, std_basis_matrix j i (φ (std_basis_matrix i j 1)).
Equations
- φ.matrix = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), matrix.std_basis_matrix j i (⇑φ (matrix.std_basis_matrix i j 1))))
given any linear functional φ : M_n →ₗ[R] R, we get φ a = (φ.matrix ⬝ a).trace.
we linear maps φ_i : M_[n_i] →ₗ[R] R, we define its direct sum as the linear map (Π i, M_[n_i]) →ₗ[R] R.
for direct sums, we get φ x = ∑ i, ((φ i).matrix ⬝ x i).trace
Any linear functional $f$ on $M_n$ is given by a unique matrix $Q \in M_n$ such that $f(x)=\operatorname{Tr}(Qx)$ for any $x \in M_n$.
⨁_i φ_i ι_i (x_i) = φ_i (x_i)
A linear functional $φ$ on $M_n$ is positive if $0 ≤ φ (x^*x)$ for all $x \in M_n$.
Equations
- φ.is_pos_map = ∀ (a : A), 0 ≤ ⇑φ (has_star.star a * a)
A linear functional $φ$ on $M_n$ is unital if $φ(1) = 1$.
A linear functional is called a state if it is positive and unital
Equations
- φ.is_state = (φ.is_pos_map ∧ φ.is_unital)
A linear functional $f$ on $M_n$ is said to be faithful if $f(x^*x)=0$ if and only if $x=0$ for any $x \in M_n$.
Equations
- φ.is_faithful = ∀ (a : A), ⇑φ (has_star.star a * a) = 0 ↔ a = 0
A linear functional $f$ is positive if and only if there exists a unique positive semi-definite matrix $Q\in M_n$ such $f(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.
A linear functional $f$ is a state if and only if there exists a unique positive semi-definite matrix $Q\in M_n$ such that its trace equals $1$ and $f(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.
A positive linear functional $f$ is faithful if and only if there exists a positive definite matrix such that $f(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.
Equations
- φ.is_faithful_pos_map = (φ.is_pos_map ∧ φ.is_faithful)
Instances for module.dual.is_faithful_pos_map
A linear functional $φ$ is a faithful and positive if and only if there exists a unique positive definite matrix $Q$ such that $φ(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.
A state is faithful $f$ if and only if there exists a unique positive definite matrix $Q\in M_n$ with trace equal to $1$ and $f(x)=\operatorname{Tr}(Qx)$ for all $x \in M_n$.
A linear functional $f$ is tracial if and only if $f(xy)=f(yx)$ for all $x,y$.
A linear functional is tracial and positive if and only if there exists a non-negative real $α$ such that $f\colon x \mapsto \alpha \operatorname{Tr}(x)$.
A linear functional is tracial and positive if and only if there exists a unique non-negative real $α$ such that $f\colon x \mapsto \alpha \operatorname{Tr}(x)$.
A linear functional $f$ is tracial positive and faithful if and only if there exists a positive real number $\alpha$ such that $f\colon x\mapsto \alpha \operatorname{Tr}(x)$.
A linear functional $f$ on $M_n$ is positive and faithful if and only if $(x,y)\mapsto f(x^*y)$ defines an inner product on $M_n$.
Equations
- module.dual.is_faithful_pos_map.inner_product_space = inner_product_space.of_core {to_has_inner := {inner := λ (x y : matrix n n ℂ), ⇑φ (x.conj_transpose.mul y)}, conj_symm := _, nonneg_re := _, definite := _, add_left := _, smul_left := _}
Equations
- module.dual.pi.inner_product_space = inner_product_space.of_core {to_has_inner := {inner := λ (x y : Π (i : k), matrix ((λ (i : k), s i) i) ((λ (i : k), s i) i) ℂ), finset.univ.sum (λ (i : k), has_inner.inner (x i) (y i))}, conj_symm := _, nonneg_re := _, definite := _, add_left := _, smul_left := _}