Compositional thermostatics
“modern math to make the foundations of Thermodynamics more precise.”
class state := sorry
def entropy [state s] : extended_real_number := sorry
class convex_space (α : Type) :=
(cλ : α → α → α)
(c1 : c1 x y = x)
(cl_x_x : cλ x x = x)
(cl_x_y : cλ x y = c{1-λ} y x)
(cλcμ_x_y_z : cλ(cμ(x,y),z) = ...)
/--
"A thermostatic system (X,S)
is a convex space X together with a concave function S : X → R,
where R has the convex structure given in Example 6.
We call X the state space,
call points of X states,
and call S the entropy function."
-/
class thermostatic_system (T : type) :=
(a convex space of states together)
(a concave function λ state s, entropy s)
Example 2. Any vector space is a convex space with the convex structure cλ(x, y) =
λx+(1−λ)y.
“This definition applies to classical thermodynamics, classical statistical mechanics, quantum statistical mechanics, and also generalized probabilistic theories of the sort studied in quantum foundations.
It also allows us to treat a heat bath as a thermostatic system on an equal footing with any other.
We construct an operad whose operations are convex relations from a product of convex spaces to a single convex space. And prove that thermostatic systems are algebras of this operad.
“Our approach requires an abstract kind of convex space. that need not be a subset of a vector space.
This gives a general formalism for combining thermostatic systems.
The formalism captures the fact that such systems maximize entropy subject to whatever constraints are imposed upon them.”
“Intuitively speaking, the operad has as operations all possible ways of combining thermostatic systems.
there is an operation that combines two gases s.t. they can exchange energy and volume, but not particles.
And another operation that lets them exchange only particles,
and so on.”
applications:
“two cylinders of ideal gas. a divider between them; movable; permeable to heat. this is an operation in an operad. if you tell us the entropy function of each cylinder of gas, our formalism will automatically compute the entropy function of the resulting combination of these two cylinders.”
the entropy maximization principle for general thermostatic systems,
“Whenever several such systems are combined and allowed to come to equilibrium, the new equilibrium state maximizes the total entropy subject to constraints.”
“the ‘canonical ensemble’, the ‘microcanonical ensemble’, or the ‘grand canonical ensemble’ in Classical statistical mechanics
“Example 13. ideal gas. state space X = ℝ³₊. coordinates (U,V,N) describe the energy, volume, and particle number of the gas. The entropy S : X → ℝ is given by the Sackur–Tetrode equation.”
“Example 16. a thermostatic system whose state space is the set of probability distributions on {0,...,n}. The natural choice of entropy function here is the Shannon entropy.”
“Example 17. More generally, for any measure space (X,μ) the set of probability distributions P(X,μ) is a convex set, and this becomes a thermostatic system with entropy function S : P (X, μ) → ℝ given by …”
“Example 19. For any Hilbert space H, let X be the set of density matrices on H, i.e. nonnegative self-adjoint operators ρ with Tr(ρ) = 1. Then this becomes a thermostatic system with entropy function S : X → ℝ given by the von Neumann entropy.”
“More generally still, concave entropy functions can be defined on the convex spaces of states in a large class of ‘generalized probabilistic theories’, making them into thermostatic systems.”
“The coarse-grained measurement”
“a system in thermodynamic equilibrium. maximizes entropy. subject to the constraints imposed on its states. The key insight behind our approach is that the constraints used in entropy maximization are typically parameterized. For instance, in a the system with two components that are constrained to have a fixed total energy, the total energy parameterizes this constraint. The formal structure that describes a parameterized collection of constraints is a convex relation R ⊆ X × Y. This convex relation assigns to each y ∈ Y a constrained set {x ∈ X | (x, y) ∈ R}.”
“Recall that convex spaces and convex relations form a category ConvRel. We use this category to formalize this application of the maximum entropy principle by constructing a functor Ent: ConvRel → Set sending any convex space X to the set of all concave functions S : X → ℝ.”