1. Physlib
  2. Thermodynamics
  3. IdealGas
  4. Basic
Imports
/- Copyright (c) 2025 Fabio Anza. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mitch Scheffer, Fabio Anza -/ module public import Mathlib.Analysis.SpecialFunctions.Pow.Real -- for Real.rpow_def_of_pos

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:

      c \log(U_a/U_b) + \log(V_a/V_b) = 0,

      (U_a/U_b)^c (V_a/V_b) = 1,

      U_a^c V_a = U_b^c V_b (the latter follows from (2)).

@[expose] public section

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)).

def entropy (c R s0 U0 V0 N0 : ℝ) (U V N : ℝ) : ℝ := N * s0 + N * R * (c * log (U / U0) + log (V / V0) - (c + 1) * log (N / N0))

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.

s0:ℝU0:ℝV0:ℝN0:ℝc:ℝR:ℝUa:ℝUb:ℝVa:ℝVb:ℝN:ℝhUa:0 < UahUb:0 < UbhVa:0 < VahVb:0 < VbhN:0 < NhU0:0 < U0hV0:0 < V0hR:0 < RhS:N * s0 + N * R * (c * (log Ua - log U0) + (log Va - log V0) - (c + 1) * log (N / N0)) = N * s0 + N * R * (c * (log Ub - log U0) + (log Vb - log V0) - (c + 1) * log (N / N0))key:N * R * (c * (log Ua - log Ub) + (log Va - log Vb)) = 0⊢ c * (log Ua - log Ub) + (log Va - log Vb) = 0 All goals completed! 🐙

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

All goals completed! 🐙