def
definition
einsteinFunction
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Thermodynamics.HeatCapacity on GitHub at line 132.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
129
130 Reproduces high-T limit (Dulong-Petit: C_V = 3R).
131 But gets low-T wrong (goes to 0 too fast). -/
132noncomputable def einsteinFunction (x : ℝ) : ℝ :=
133 x^2 * exp x / (exp x - 1)^2
134
135noncomputable def einsteinCv (omega_E T : ℝ) (hT : T > 0) : ℝ :=
136 3 * R_gas_constant * einsteinFunction (hbar * omega_E / (kB_SI * T))
137
138/-! ## Debye Model -/
139
140/-- Debye model for solids:
141
142 Distribution of frequencies up to cutoff ω_D.
143 Density of states: g(ω) ∝ ω²
144
145 C_V = 9R (T/Θ_D)³ ∫₀^(Θ_D/T) x⁴eˣ/(eˣ-1)² dx
146
147 Low T: C_V ∝ T³ (matches experiment!)
148 High T: C_V → 3R (Dulong-Petit)
149
150 The T³ law is the key success. -/
151noncomputable def debyeTemperature (omega_D : ℝ) : ℝ := hbar * omega_D / kB_SI
152
153/-- Debye T³ law at low temperature:
154
155 C_V = (12π⁴/5) R (T/Θ_D)³
156
157 This is EXACT as T → 0.
158
159 In RS: The T³ comes from 3D × ω² density of states.
160 The 3D is essential! -/
161noncomputable def debyeT3Coefficient : ℝ := 12 * pi^4 / 5
162