QuantumInfo.StatMech.Hamiltonian

Let $D$ be a type of parameters and $H$ be a microcanonical Hamiltonian (of type `MicroHamiltonian D`). For any parameter $d \in D$, the dimension of the state space associated with that parameter, denoted as $H.\text{dim}(d)$, is a finite set (represented by the typeclass `Fintype`). This definition provides an instance to the global cache ensuring that finite measures and other properties requiring finiteness can be automatically synthesized for these dimensions.

The standard microcanonical ensemble Hamiltonian, denoted as $NVE\text{Hamiltonian}$, is a `MicroHamiltonian` where the underlying state space (or data type) $D$ is defined as the Cartesian product $\mathbb{N} \times \mathbb{R}$. Here, a state is represented by a pair $(N, V)$, where $N \in \mathbb{N}$ denotes the total number of particles and $V \in \mathbb{R}$ denotes the volume of the system.

Given an $N-V$ Hamiltonian state represented as a pair $(N, V) \in \mathbb{N} \times \mathbb{R}$, where $N$ is the number of particles and $V$ is the volume, this function extracts the first component of the pair to return the number of particles $N$.

Given an $N-V$ Hamiltonian state represented as a pair $(N, V) \in \mathbb{N} \times \mathbb{R}$, where $N$ is the number of particles and $V$ is the volume, this function extracts the second component of the pair to return the volume $V$.