Ideal gas: basic entropy and adiabatic relations

In this module we formalize a simple thermodynamic model of a monophase ideal gas. We:

• Define the entropy S(U,V,N) = N s₀ + N R (c \log(U/U₀) + \log(V/V₀) - (c+1)\log(N/N₀)),

• Prove equivalent formulations of the adiabatic relation for two states (U_a, V_a) and (U_b, V_b) at fixed N:

  1. c \log(U_a/U_b) + \log(V_a/V_b) = 0,
  2. (U_a/U_b)^c (V_a/V_b) = 1,
  3. U_a^c V_a = U_b^c V_b (the latter follows from (2)).

def entropy (c R s0 U0 V0 N0 U V N : ℝ) : ℝ

Entropy of a monophase ideal gas: S(U,V,N) = N s0 + N R (c log(U/U0) + log(V/V0) - (c+1) log(N/N0)).

Equations

• entropy c R s0 U0 V0 N0 U V N = N * s0 + N * R * (c * Real.log (U / U0) + Real.log (V / V0) - (c + 1) * Real.log (N / N0))

theorem adiabatic_relation_log {s0 U0 V0 N0 c R Ua Ub Va Vb N : ℝ} (hUa : 0 < Ua) (hUb : 0 < Ub) (hVa : 0 < Va) (hVb : 0 < Vb) (hN : 0 < N) (hU0 : 0 < U0) (hV0 : 0 < V0) (hR : 0 < R) (hS : entropy c R s0 U0 V0 N0 Ua Va N = entropy c R s0 U0 V0 N0 Ub Vb N) : c * Real.log (Ua / Ub) + Real.log (Va / Vb) = 0

Adiabatic relation in logarithmic form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then c * log (Ua/Ub) + log (Va/Vb) = 0.

theorem adiabatic_relation_UaUbVaVb {s0 U0 V0 N0 c R Ua Ub Va Vb N : ℝ} (hUa : 0 < Ua) (hUb : 0 < Ub) (hVa : 0 < Va) (hVb : 0 < Vb) (hN : 0 < N) (hU0 : 0 < U0) (hV0 : 0 < V0) (hR : 0 < R) (hS : entropy c R s0 U0 V0 N0 Ua Va N = entropy c R s0 U0 V0 N0 Ub Vb N) : (Ua / Ub).rpow c * (Va / Vb) = 1

Adiabatic relation in product form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then (Ua/Ub)^c * (Va/Vb) = 1.