Maxwell relation

Stream: new members

[Parivash]

Hi,
I'm going to prove the following rule:
Definition: $dU=TdS - PdV$. We can now consider U as a function of S and V such that U=U(S,V).
We can now write the total differential of U=U(S,V) as:
$dU=(\frac{\partial U}{\partial S})_{V} dS+(\frac{\partial U}{\partial V})_{S} dV$
We can now equate the two expression for dU:
$dU=(\frac{\partial U}{\partial S})_{V} dS+(\frac{\partial U}{\partial V})_{S} dV = TdS-PdV$
From here we can equate the coefficients of dS and dV:
$(\frac{\partial U}{\partial S})_{V}=T$
$(\frac{\partial U}{\partial V})_{S}=-P$
Let's only consider the first of these $(\frac{\partial U}{\partial S})_{V}=T$. Consider here differentiating both sides with respect to V while keeping S constant. This means we apply$$ (\frac{\partial}{\partial V})_{S}$$ to both sides, such that:
$\frac{\partial}{\partial V})_{S}(\frac{\partial U}{\partial S})_{V}= (\frac{\partial T}{\partial V})_{S}$
again consider differentiating both sides of $(\frac{\partial U}{\partial V})_{S}=-P$ with respect to S while keeping V constant. This means applying $\frac{\partial}{\partial S})_{V}$ to both sides:
$\frac{\partial}{\partial S})_{V}(\frac{\partial U}{\partial V})_{S} = -(\frac{\partial P}{\partial S})_{V}$

• we can flip the order here like:
  $\frac{\partial}{\partial S})_{V}\frac{\partial}{\partial V})_{S}U = \frac{\partial}{\partial V})_{S}\frac{\partial}{\partial S})_{V}U$
  So, from the two result above we have:
  $(\frac{\partial T}{\partial V})_{S}=-(\frac{\partial P}{\partial S})_{V}$
  I appreciate to get some help understanding how to formalize this rule by Lean
  Thanks

[Kevin Buzzard]

Do we have differential forms in the sense of differential geometry yet?

[Parivash]

@Kevin Buzzard
Professor Kevin, not sure I could understand your means.
So, you means Lean not support to formalize it or I should explain it in the other ways

[Kevin Buzzard]

I mean "can you state what you want to prove in Lean"? Stating the theorem is a necessary prerequisite for proving it, and I am raising the possibility that it might be nontrivial to even state, given what we have right now -- or I might be wrong.

[Kevin Buzzard]

Basically, you are not really asking a well-formed question right now. "Can you prove <maths stuff> in Lean" is ambiguous. "Can you prove <lean code with a sorry in>" is not.

[Yaël Dillies]

To be fair to Parivash, they asked "how to formalize this rule in Lean" which includes stating the theorem. But I agree it's no easy task.

[Parivash]

Yeah, your right I don't clearly separate goals ,...
This is our goal: $(\frac{\partial T}{\partial V})_{S}=-(\frac{\partial P}{\partial S})_{V}$
In order to prove it we need to use
1st) this definition: $dU=TdS-PdV$
2nd) from the 1st we find that U is dependent on S and V (U=U(S,V))
So, by following the mentioned path finally we could reach the goal.

[Kevin Buzzard]

What I'm trying to say is that you can talk as much maths as you like, but without some Lean code it's very difficult to engage with the questions you're asking.

[Kevin Buzzard]

With your earlier questions about infinite sums of real numbers it was easy to translate the maths into Lean so this was not an issue. But with differentials it's a different story.

[Parivash]

Yeah, exactly, that's totally different!
Let me see how can I define it in Lean to provide you

[Kevin Buzzard]

And what I am concerned about is that although mathlib has the real numbers, I am unclear about whether it has differential forms right now (I know people are working on it but I don't know if we're there yet) so any Lean statement might have to avoid differential forms (mathlib does have partial derivatives though).

[Parivash]

Ooooh, Thank you!

[Patrick Massot]

Parivash said:

Hi,
I'm going to prove the following rule:
Definition: $dU=TdS - PdV$. We can now consider U as a function of S and V such that U=U(S,V).

Lean cannot help you if you don't have a mathematical definition and a mathematical statement. Your "definition" is meaningless. At the very least you need to specify the types of U, T, P, V and S before writing anything else.

[Patrick Massot]

I know this isn't the rule of the game in physics. And I have nothing against physics, but this is not the game you can play with Lean.

[Tomas Skrivan]

Bellow is a sketch how to do it in Lean 4. Maxwell relations are just a simple consequence of the fact that you can swap partial derivatives.

<rant> I would advocate to drop all the nonsense with differentials, which I think is a crime on poor physics students. All those differentials are never well explained and just plain confusing. </rant>

As a starting point, I would just define temperature as $T = \frac{\partial U}{\partial S}$ and pressure as $P = -\frac{\partial U}{\partial V}$ then the first Maxwell relation is just swapping partial derivatives.

The other relations are a bit trickier. You perform Legendre transform on the internal energy $U$ to switch to different set of variables. For example, for the second Maxwell's relation the hardest part is to show that the temperature is related to enthalphy as $T = \frac{\partial H}{\partial S}$ and that volume is related to enthalphy as $V = \frac{\partial H}{\partial P}$ (theorems enthalpy_temperature and enthalpy_volume). Once you have these relations, it is again just swapping partial derivatives.

One of the most confusing part when learning thermodynamics is that the book/lecture randomly jumps between different set of variables. Sometime they talk about temperature as a function of entropy and pressure but sometimes temperature as a function of entropy and volume. In Lean, you have to be very explicit about this and you can't just jump between variables like this. Thus in the code bellow I have two separate function T_sp and T_sv to denote temperature as a function of different sets of variables.

Here is the Lean 4 sketch:

The notation ⅆ (x':=x), f x' corresponds to the mathematical $\frac{d f(x')}{d x'} \big|_{x'=x}$

-- necessary operations
abbrev ℝ := Float

def inverse (f : α → β) : β → α := sorry
postfix:max (priority:=high) " ⁻¹ " => inverse

def derivative (f : ℝ → ℝ) : ℝ → ℝ := sorry
macro (priority:=high) " ⅆ " "(" x:ident ":=" xval:term ")" "," fval:term : term => `((derivative λ $x => $fval) $xval )



-- internal energy -------------------------------------------------------------
def U (S : ℝ) (V : ℝ) : ℝ := sorry

-- definition of temperature and pressure as functions of entropy and volume
def T_sv (s v) := ⅆ (s':=s), U s' v
def P_sv (s v) := - ⅆ (v':=v), U s v'


theorem MaxwellRelation1 (s v)
  : (ⅆ (v':=v), T_sv s v') = - (ⅆ (s':=s), P_sv s' v) :=
by
  unfold T_sv P_sv
  -- swap derivatives and we are done
  admit

-- Enthalpy --------------------------------------------------------------------

-- volume and temperature as functions of entropy and pressure
-- change of variables comming from Legandre transform
def V_sp (s p : ℝ) := (λ v => P_sv s v)⁻¹ p
def T_sp (s p : ℝ) := T_sv s (V_sp s p)

-- Enthalpy
-- H is leganre transform of U w.r.t. to V variable
def H (s p : ℝ) : ℝ := U s (T_sp s p) - p * T_sp s p

theorem enthalpy_temperature (s p) : T_sp s p = (ⅆ (s':=s), H s' p) := sorry
theorem enthalpy_volume      (s p) : V_sp s p = (ⅆ (p':=p), H s p') := sorry

theorem MaxwellRelation2 (s p)
  : (ⅆ (p':=p), T_sp s p') = (ⅆ (s':=s), V_sp s' p) :=
by
  simp only [enthalpy_temperature, enthalpy_volume]
  -- swap derivatives and we are done
  admit


-- Helmholtz -------------------------------------------------------------------

-- entropy and pressure as functions of temperature and volume
def S_tv (t v : ℝ) := (λ s => T_sv s v)⁻¹ t
def P_tv (t v : ℝ) := P_sv (S_tv t v) v


-- Helmholtz free energy
-- F is leganre transform of U w.r.t. to S variable
def F (t v : ℝ) : ℝ := U (S_tv t v) v - t * S_tv t v

theorem helmholtz_pressure (t v : ℝ) : P_tv t v = - (ⅆ (v':=v), F t v') := sorry
theorem helmholtz_entropy  (t v : ℝ) : S_tv t v = - (ⅆ (t':=t), F t' v) := sorry

theorem MaxwellRelation3 (t v)
  : (ⅆ (v':=v), S_tv t v') = (ⅆ (t':=t), P_tv t' v) :=
by
  simp only [helmholtz_pressure,helmholtz_entropy]
  -- swap derivatives and we are done
  admit