structure MicroHamiltonian (D : Type) : Type 1

The Hamiltonian for a microcanonical ensemble, parameterized by any extrinsic parameters of data D. Since it's an arbitrary type, 'T' would be nice, but we use 'D' for data to avoid confusion with temperature. We define Hamiltonians as an energy function on a real manifold, whose dimension n possibly depends on the data D. Energy is a WithTop ℝ, ⊤ is used to mean "excluded as a possibility in phase space". This formalization does exclude the possibility of discrete degrees of freedom; it is not completely general. A better formalization could have an arbitrary measurable space.

• dim : D → Type
• dim_fin (d : D) : Fintype (self.dim d)
• H {d : D} : (self.dim d → ℝ) → WithTop ℝ

instance microHamiltonianFintype {D : Type} (H : MicroHamiltonian D) (d : D) : Fintype (H.dim d)

We add the dim_fin to the instance cache so that things like the measure can be synthesized

Equations

• microHamiltonianFintype H d = H.dim_fin d

@[reducible, inline]

abbrev NVEHamiltonian : Type 1

The standard microcanonical ensemble Hamiltonian, where the data is the particle number N and the volume V.

Equations

• NVEHamiltonian = MicroHamiltonian (ℕ × ℝ)

def NVEHamiltonian.N : ℕ × ℝ → ℕ

Helper to get the number in an N-V Hamiltonian

Equations

• NVEHamiltonian.N = Prod.fst

def NVEHamiltonian.V : ℕ × ℝ → ℝ

Helper to get the volume in an N-V Hamiltonian

Equations

• NVEHamiltonian.V = Prod.snd