We unify the Henstock-Kurzweil treatment of open quantum systems with bosonic Gaussian reservoirs and fermionic Grassmann reservoirs. Finite cylindrical gauge integrals yield determinant and covariance identities for bosons, while Berezin integration yields Pfaffian identities for fermions. In both sectors the reservoir is eliminated into an influence functional and the reduced dynamics is organised by Chernoff splitting. The accompanying Lean 4 developments verify the finite-dimensional Gaussian, operator, exterior-algebra, and Pfaffian steps. This upload contains the paper and the accompanying Lean 4 formalisation. The Lean development is free of sorry, admit, and newly introduced axioms. Kernel axiom inspection of the headline results reports only propext, Classical.choice, and Quot.sound. The finite-mode formulas are exact and machine-checked; continuum and unbounded-generator qualifications are kept explicit in the paper.
We unify the Henstock-Kurzweil treatment of open quantum systems with bosonic Gaussian reservoirs and fermionic Grassmann reservoirs. Finite cylindrical gauge integrals yield determinant and covariance identities for bosons, while Berezin integration yields Pfaffian identities for fermions. In both sectors the reservoir is eliminated into an influence functional and the reduced dynamics is organised by Chernoff splitting. The accompanying Lean 4 developments verify the finite-dimensional Gaussian, operator, exterior-algebra, and Pfaffian steps. This upload contains the paper and the accompanying Lean 4 formalisation. The Lean development is free of sorry, admit, and newly introduced axioms. Kernel axiom inspection of the headline results reports only propext, Classical.choice, and Quot.sound. The finite-mode formulas are exact and machine-checked; continuum and unbounded-generator qualifications are kept explicit in the paper.
This preprint develops a rigorous, machine-checked construction of non-Gaussian functional integrals using the Henstock–Kurzweil (HK) gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with an action containing a quartic self-interaction λ∑iφi4λ∑iφi4. We show that the one-mode non-Gaussian integral is finite, positive, monotone and infinitely differentiable in the coupling λλ on [0,∞)[0,∞), with derivatives given by convergent integrals rather than by the divergent perturbative series. The MM-mode influence functional factorises into one-mode integrals and is bounded by its Gaussian value. A Chernoff/Lie–Trotter splitting handles non-commutativity of the free and non-Gaussian generators. All statements are formalised in Lean 4 / Mathlib and are free of sorry, using only the standard axioms propext, Classical.choice, Quot.sound. The accompanying Lean file HkNonGaussian.lean is included. Illustrative applications are worked out at the level of explicit formulas: the Duffing oscillator, local volatility (CEV) in finance, Wilson–Cowan neural fields, and non-Gaussian quantum reservoirs. This work is a direct continuation of the author’s programme on machine-verified path integrals without Wick rotation.
Developing numerical exact solvers for open quantum systems is a challenging task due to the non-perturbative and non-Markovian nature when coupling to structured environments. The Feynman-Vernon influence functional approach is a powerful analytical tool to study the dynamics of open quantum systems. Numerical treatments of the influence functional including the quasi-adiabatic propagator technique and the tensor-network-based time-evolving matrix product operator method have proven to be efficient in studying open quantum systems with bosonic environments. However, the numerical implementation of the fermionic path integral suffers from the Grassmann algebra involved. In this work, we present a detailed introduction to the Grassmann time-evolving matrix product operator method for fermionic open quantum systems. In particular, we introduce the concepts of Grassmann tensor, signed matrix product operator, and Grassmann matrix product state to handle the Grassmann path integral. Using the single-orbital Anderson impurity model as an example, we review the numerical benchmarks for structured fermionic environments for real-time nonequilibrium dynamics, real-time and imaginary-time equilibration dynamics, and its application as an impurity solver. These benchmarks show that our method is a robust and promising numerical approach to study strong coupling physics and non-Markovian dynamics. It can also serve as an alternative impurity solver to study strongly correlated quantum matter with dynamical mean-field theory.
The methods that have been described in previous chapters can be used to study general quantum Bose systems. They are based in a direct way on the introduction of a generating function of symmetric wave functions of bosons. In the case of fermion systems, however, one faces the problem that fermion wave functions, or fermion correlation functions (or Green functions) are antisymmetric with respect to the exchange of a fermion pair. Thus, the construction of generating functions requires the introduction of an antisymmetric or Grassmann algebra of ‘classical functions’. It is then possible to generalize to Grassmann algebras the notions of derivatives and integrals, yielding quite parallel formalisms for bosons and fermions, in particular, to define a path integral for fermion systems, analogous to the holomorphic path integral for bosons. This chapter discusses differentiation and integration in Grassmann algebras, Gaussian integrals and perturbative expansion, partition function, and quantum Fermi gas.
Abstract In this work, the perturbative aspects of quantum mechanics (QM) and quantum field theory (QFT), to a large extent, are studied with functional (path or field) integrals and functional techniques. This physics textbook thus begins with a discussion of algebraic properties of Gaussian measures, and Gaussian expectation values for a finite number of variables. The important role of Gaussian measures is not unrelated to the central limit theorem of probabilities, although the interesting physics is generally hidden in essential deviations from Gaussian distributions. A few algebraic identities about Gaussian expectation values, in particular Wick's theorem are recalled. Integrals over some type of formally complex conjugate variables, directly relevant for boson systems are defined. Fermion systems require the introduction of Grassmann or exterior algebras, and the corresponding generalization of the notions of differentiation and integration. Both for complex and Grassmann integrals, Gaussian integrals, and Gaussian expectation values are calculated, and generalized Wick's theorems proven. The concepts of generating functions and Legendre transformation are recalled.
The aim of this paper is to give a self-contained and unified presentation of a fermionic coherent state theory with the necessary mathematical details, discussing their definition, properties and some applications. After defining Grassmann algebras, it is possible to get a classical analog for the fermionic degrees of freedom in a quantum system. Following the basic work of Berezin (1966 The Method of Second Quantization (New York: Academic); 1987 Introduction to Superanalysis (Dordrecht: Reidel Publishing Company)), we show that we can compute with Grassmann numbers as we do with complex numbers: derivation, integration, Fourier transform. After that we show that we have quantization formulas for fermionic observables. In particular, there exists a Moyal product formula. As an application, we consider explicit computations for propagators with quadratic Hamiltonians in annihilation and creation operators. We prove a Mehler formula for the propagator and Mehlig–Wilkinson-type formulas for the covariant and contravariant symbols of ‘metaplectic’ transformations for fermionic states. This article is part of a special issue of Journal of Physics A: Mathematical and Theoretical devoted to ‘Coherent states: mathematical and physical aspects’.
Dynamics of open quantum systems with structured reservoirs can often be simulated efficiently with tensor network influence functionals. The standard variants of the time-evolving matrix product operator (TEMPO) method are applicable when the systems is coupled to Gaussian bosonic baths via hermitian coupling operators that mutually commute. In this work we introduce a generalization to cases where the system is coupled to a single reservoir through multiple non-commuting operators, representing the most general form of linear system-bath coupling. We construct a Gaussian influence functional that properly handles Trotter errors arising from a finite evolution time step, thus ensuring convergence for long evolution times. Based on this result, the uniform TEMPO scheme can be employed to obtain a matrix product operator form of the influence functional, enabling efficient simulations of the real-time dynamics of the open system. As a demonstration, we simulate the time evolution of driven two-level emitters coupled to a bosonic lattice at different lattice sites.