Papers With

← All papers
First page of Optimal Linear Combination of Hamiltonian Simulation for Dissipative Dynamics

Optimal Linear Combination of Hamiltonian Simulation for Dissipative Dynamics

Hongkang Ni, Lexing Ying

quant-ph Oct 29, 2026 · v1
formalization mathlib quantum analysis
Read PDF arXiv abstract Code
TL;DR
The main minimax theorem (Theorem 1.1) on the optimal LCHS error is formalized and checked in Lean 4 with Mathlib, developed with AI assistance.
Abstract
Linear combination of Hamiltonian simulation (LCHS) is an efficient method for simulating dissipative dynamics on quantum computers. The choice of the LCHS kernel controls the cost of the algorithm. We prove that the kernel family proposed by Ni and Ying \cite{NY26} minimizes the LCHS query cost in the minimax sense. For target accuracy $ε$, the minimum cost is asymptotically $\frac{2\mathrm{e}}π(\ln\frac1ε-\ln\ln\frac1ε+o(1))$, with optimal leading constant $\frac{2\mathrm{e}}π$. Our lower-bound proof combines weak duality with a realization lemma that approximates extremal dual functions by matrix elements of dissipative evolutions.
Problem

Linear combination of Hamiltonian simulation (LCHS) simulates dissipative dynamics on quantum computers. Its query cost depends on the choice of kernel. The open question was whether the Ni–Ying kernel family is optimal for the cost λR.

Approach

The minimax error over measures with support in [-R,R] and total variation at most λ is characterized exactly. For the lower bound, weak duality is combined with a realization lemma that approximates extremal dual functions by matrix elements of dissipative evolutions. The realization uses polynomial approximation, time-ordered evolutions, a clock register and clock discretization. The upper bound comes from the Ni–Ying local Wiener norm estimates. Theorem 1.1 was formalized in Lean 4 with Mathlib.

Results

The minimal error is V_R(λ), given in closed form. The optimal cost is (2e/π)(ln(1/ε) − ln ln(1/ε)) + o(1), so the leading constant 2e/π is optimal. The formal Lean proof uses only Lean's standard axioms.