Simulation ยท Analysis
First-order Trotter bound
Theorem statement
Let $d\geq0$ be an integer, $t\geq0$ be real,
and $H_1,H_2\in\mathbb{C}^{d\times d}$
be Hermitian matrices.
Then
$$
\left\|
e^{-it(H_1+H_2)}-e^{-itH_1}e^{-itH_2}
\right\|
\leq
\frac{t^2}{2}\left\|H_1H_2-H_2H_1\right\|,
$$
where
$\|M\|=\sup\{\|Mv\|_2:v\in\mathbb{C}^d,\ \|v\|_2\leq1\}$.
Sources
Lean context
- Lean declaration
QuantumAlg.TrotterOneStepErrorBound.oneStep_error_bound
Copy a short prompt with the import, theorem name, citations, and public source link.