computing of parameterized operators

Stream: general

[Richard Ruan]

Hi, I am a researcher in quantum computing. I met a problem of simplifying parameterized operators. The simplification involves calculating the partial derivative of the parameterized operators, which is particularly complicated after expansion. In the case of hand calculation, I can only get a satisfactory reduction form if the parameters take some specific values.
A few days before, I read an introductory article for LEAN, and thought LEAN could be a great tool for simplifying parameterized operators.  However, after learning LEAN for a few days, I am not sure if LEAN is suitable for solving my problems. Can someone help me to address this issue? I really appreciate any help provided.

[Bbbbbbbbba]

Could you give a concrete example to illuminate your use case?

[Yaël Dillies]

Currently, there is not a huge lot of machinery to do computations in Lean. There is no particular limitation why*, simply that no one has had the need for it. It will certainly change over time (and you can help make it happen!) and then you will be able to compute parametrised operators.

*There is one reason, at least when compared to eg Isabelle: Lean is a dependent type theory, so unification (the act of assigning metavariables given the existing context) is much harder than in a simple type theory. As a result, it is less straightforward to write automation. It is nevertheless not impossible.

[Richard Ruan]

Thanks for your attention. Here is an example of my question:

$$H(t) = \lambda(t) H_T + (1-\lambda(t))H_S;\\ A(\alpha) = i \alpha_0 [H, \partial_\lambda H] + i \alpha_1[H, [H, [H, \partial_\lambda H] ] ] + \dots$$

where $H_S$ and $H_T$ refer to the initial Hamiltonian and final Hamiltonian (Hermitian matrices) of a quantum system. I want to simplify $A(\alpha)$ with parameters $\alpha$ and $\lambda$.

[Richard Ruan]

$H_s$ and $H_T$ can be described (decomposed) by the Kronecker product of Pauli matrices. For a particular quantum system, there are many opportunities to cancel and merge the components of these matrices. For a simple example, $X Y =i Z$. But when the expanded expression has hundreds of terms, simplifying manually is exhausting and easy to have errors. I am wondering can LEAN help me automatically do this task?

[Yaël Dillies]

So the expanded expression has indeed finitely terms?

[Richard Ruan]

Yes. It only has fintiely terms.