PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Quadratic.Operational

Composing quadratic operations

i. Overview

For quadratically positive Jordan algebras the positive maps `U_a` compose according to the fundamental formula.

ii. Key results

- `JordanAlgebra.quadRepPositiveLinearMap_fundamental` : the fundamental formula for the positive maps `U_a`.

2 declarations

theorem

$U_{a^2} = U_a \circ U_a$

#quadRepPositiveLinearMap_mul_self

For any element $a$ in a Jordan algebra $E$ , the quadratic representation $U_{a^2}$ of the square $a^2$ is equal to the composition of the quadratic representation $U_a$ with itself: $U_{a^2} = U_a \circ U_a$ where $U_x$ denotes the positive linear map corresponding to the quadratic representation of an element $x \in E$ .

theorem

Fundamental Formula for Jordan Algebras: $U_{U_a(b)} = U_a \circ U_b \circ U_a$

#quadRepPositiveLinearMap_fundamental

Let $E$ be a Jordan algebra. For any elements $a, b \in E$ , the quadratic representation of the element $U_a(b)$ satisfies the fundamental formula: $U_{U_a(b)} = U_a \circ U_b \circ U_a$ where $U_x: E \to E$ denotes the quadratic representation of an element $x$ , defined by $U_x(y) = 2x \circ (x \circ y) - (x^2 \circ y)$ .