Thermal state

/-- thermal equilibrium at inverse temperature β -/
def thermal_state := 
e^(−β HB) / Z

def Z : ℝ :=
∑ i, exp(-β*(E i))

/-- "Appending a thermal state
is a reversible thermal operation." -/
lemma appending_thermal_state_is_reversible_thermal :
  ... :=
sorry