Ordered Three-Pulse Trace

Abstract

Ordered three-pulse trace deviation has a dimension-free Frobenius bound.

Definition 1.1 (The matrix pulse integral).

$$D_X(s)={\int }_0^1\exp irsXXdr$$

Formalization. D5/S3/Quantum/Dynamics/OrderedThreePulseTrace.pulse0 (✓ std3).

Source. Repository-derived.

Commentary.

For every finite index type, complex square matrix X and real s, the pulse is the interval integral of exp(i r s X) X over 0 <= r <= 1. The matrix product keeps X on the right.

Theorem 1.2 (Ordered three-pulse real trace bound).

$$\begin{array}{c}\forall (I:Type)[\mathrm{Fintype}(I)][\mathrm{DecidableEq}(I)],\\ \forall A,B,C:Ma{t}_I(\mathbb{R}),\forall L,t:\mathbb{R},\\ A^T=A\wedge B^T=B\wedge C^T=C\wedge \\ 0\le L\wedge \Vert A{\Vert }_F\le L\wedge \Vert B{\Vert }_F\le L\wedge \Vert C{\Vert }_F\le L\wedge 0<t\Rightarrow \\ [(\forall X:Ma{t}_I(\mathbb{C}),D_X(0)=X)\wedge \\ (\forall X:Ma{t}_I(\mathbb{C}),\forall s:\mathbb{R},s\ne 0\Rightarrow D_X(s)=\frac{\exp isX-I}{is})\wedge \\ |\Re {\mathrm{Tr}}_{\mathbb{C}}(D_{A_{\mathbb{C}}}(t)D_{B_{\mathbb{C}}}(t)D_{C_{\mathbb{C}}}(t))-{\mathrm{Tr}}_{\mathbb{R}}(ABC)|\le \frac{5}{4}{L}^5{t}^2]\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/OrderedThreePulseTrace.ordered_three_pulse_real_trace_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The index type is any finite type, including the empty type. A, B and C are real symmetric square matrices with their actual Frobenius norms at most L, where L is nonnegative; t is positive. No pairwise commutation is assumed.

The same theorem proves D_X(0) = X and, for every nonzero real s, D_X(s) = (exp(i s X) - I)/(i s), even for arbitrary complex X. In the trace bound each real matrix is entrywise complexified; the three pulse factors remain in A, B, C order.

The proof uses the existing GNS Frobenius norm-square trace identity, unitary matrix exponentials, two derivatives of the ordered product, and the nine-term second-derivative estimate. The latter is at most 5 L^5/2; the zero derivative of the real trace at zero gives the 5 L^5 t^2/4 remainder. The quotient identity follows from the interval fundamental theorem of calculus.

References

• Truth anchor: D5/S3/Quantum/Dynamics/OrderedThreePulseTrace.ordered_three_pulse_real_trace_bound
• Truth anchor: D5/S3/Quantum/Dynamics/OrderedThreePulseTrace.pulse0
• Dependency: D5/S3/Quantum/GNSMatrix