Formalising basic classical thermodynamics

Stream: new members

[Mitchell Scheffer]

Hello, I am trying to formalize some basic topics in classical thermodynamics. Is the framework in place for taking differential forms and integrating over them in mathlib? Something like

$S \equiv S(U,V,N)$ which has the differential form $dS = \dfrac{\partial S}{\partial U}dU + \dfrac{\partial S}{\partial V}dV + \dfrac{\partial S}{\partial N}dN$

I'm an undergrad in math and physics so sorry if these questions seem naive.
More specifically (getting into the weeds), I am currently trying formalize the three different forms Poisson's relation for an ideal gas which would involve defining the equations of state $PV=NRT, ~~U=cNRT$ and some thermodynamic assumptions $dU=\cancel{dQ}^{~0}+dW,~~dW=-PdV$, then taking differential forms to get $PdV + VdP = cNRdT,~~dU=cNRdT$ and then manipulating these to relationships to get something like $C\dfrac{1}{P}dP=\dfrac{1}{V}dV$ and integrating. If this sort of process is not yet possible to formalize, i would appreciate guidance on what to search for to understand the underlying math involved, thanks for your help.

[Yan Yablonovskiy 🇺🇦]

Could you first define the S, as a function with a domain and codomain. As in just where it lives. For your lemma you can use the hypothesis that that PV = NRT, etc in your lemma , as well as appropriate differentiability assumptions.

It would help a lot to have for reference a very rigorous pen and paper proof.

The first step is to state the theorems statement , and then use sorry as a placeholder, checking the definitions are doing what you expect

I think what you are trying to say is possible to formalise, but mathlib works in full generality so it would be a lot of abstract machinery applied to very specific cases.

[ZhiKai Pong]

I think the answer will vary greatly depending on what exactly you want to do. The meaning and rigor of the usage of "differential forms" by a physicist is significantly different from that of a mathematician, and you have to be quite precise about what you actually want to prove.

If you just want to show that PV=nRT implies PV^γ = const given some assumptions, it's probably not very difficult and may not require differential forms (in the mathematical sense) at all, instead it's just manipulating derivatives etc.

doing thermodynamics "properly" is an entirely different beast and my limited knowledge is that there are some very advanced manifold theory involved. Even setting this up would probably be a huge effort.

If you're just getting into this and not really sure yet, I'd also recommend checking out #PhysLean or #Natural sciences, where you may get more specific advice.

[Snir Broshi]

There's also #Quadratic Forms -- Hasse-Minkowski Theorem which might be relevant