1. Physlib
  2. Thermodynamics
  3. Temperature
  4. Basic
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module public import Mathlib.Analysis.Calculus.Deriv.Inv public import Mathlib.Analysis.InnerProductSpace.Basic public import Physlib.StatisticalMechanics.BoltzmannConstant

Temperature

In this module we define the type Temperature, corresponding to the temperature in a given (but arbitrary) set of units which have absolute zero at zero.

This is the version of temperature most often used in undergraduate and non-mathematical physics.

The choice of units can be made on a case-by-case basis, as long as they are done consistently.

@[expose] public section

The type Temperature represents the temperature in a given (but arbitrary) set of units (preserving zero). It currently wraps ℝ≥0, i.e., absolute temperature in nonnegative reals.

The nonnegative real value of the temperature.

structure Temperature where val : ℝ≥0

Coercion to ℝ≥0.

instance : Coe Temperature ℝ≥0 := ⟨fun T => T.val⟩

Topology on Temperature induced from ℝ≥0.

instance : TopologicalSpace Temperature := TopologicalSpace.induced (fun T : Temperature => (T.val : ℝ≥0)) inferInstance
instance : Zero Temperature := ⟨⟨0⟩⟩@[ext] lemma ext {T₁ T₂ : Temperature} (h : T₁.val = T₂.val) : T₁ = T₂ := T₁:TemperatureT₂:Temperatureh:T₁.val = T₂.val⊢ T₁ = T₂ T₂:Temperatureval✝:ℝ≥0h:{ val := val✝ }.val = T₂.val⊢ { val := val✝ } = T₂; val✝¹:ℝ≥0val✝:ℝ≥0h:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ }; val✝:ℝ≥0⊢ { val := val✝ } = { val := val✝ }; All goals completed! 🐙lemma β_toReal (T : Temperature) : (β T : ℝ) = 1 / (kB * (T : ℝ)) := rfllemma ofβ_eq : ofβ = fun β => ⟨⟨1 / (kB * β), β:ℝ≥0⊢ 0 ≤ 1 / (kB * ↑β) β:ℝ≥0⊢ 0 ≤ 1β:ℝ≥0⊢ 0 ≤ kB * ↑β β:ℝ≥0⊢ 0 ≤ 1 All goals completed! 🐙 β:ℝ≥0⊢ 0 ≤ kB * ↑β β:ℝ≥0⊢ 0 ≤ kBβ:ℝ≥0⊢ 0 ≤ ↑β β:ℝ≥0⊢ 0 ≤ kB All goals completed! 🐙 β:ℝ≥0⊢ 0 ≤ ↑β All goals completed! 🐙⟩⟩ := ⊢ ofβ = fun β => { val := ⟨1 / (kB * ↑β), ⋯⟩ } All goals completed! 🐙All goals completed! 🐙lemma ofβ_toReal (β : ℝ≥0) : (ofβ β).toReal = 1 / (kB * (β : ℝ)) := rflAll goals completed! 🐙

Positivity of β from positivity of temperature.

T:TemperaturehT_pos:0 < T.val⊢ 0 < 1 / (kB * T.toReal) exact one_div_pos.mpr (mul_pos kB_pos (T:TemperaturehT_pos:0 < T.val⊢ 0 < T.toReal All goals completed! 🐙))

Regularity of ofβ

hg:ContinuousOn (fun b => 1 / (kB * ↑b)) (Set.Ioi 0)hind:IsInducing fun T => T.val⊢ ContinuousOn ((fun T => T.val) ∘ ofβ) (Set.Ioi 0) hg:ContinuousOn (fun b => 1 / (kB * ↑b)) (Set.Ioi 0)hind:IsInducing fun T => T.val⊢ Set.EqOn ((fun T => T.val) ∘ ofβ) (Real.toNNReal ∘ fun b => 1 / (kB * ↑b)) (Set.Ioi 0) hg:ContinuousOn (fun b => 1 / (kB * ↑b)) (Set.Ioi 0)hind:IsInducing fun T => T.valb:ℝ≥0hb:b ∈ Set.Ioi 0⊢ ((fun T => T.val) ∘ ofβ) b = (Real.toNNReal ∘ fun b => 1 / (kB * ↑b)) b All goals completed! 🐙All goals completed! 🐙

Convergence

Eventually, ofβ β is positive as β → ∞`.

b:ℝ≥0hb:0 < bthis:0 < 1 / (kB * ↑b)⊢ (ofβ b).toReal > 0 All goals completed! 🐙

General helper: for any a > 0, we have 1 / (a * b) → 0 as b → ∞ in ℝ≥0.

private lemma tendsto_const_inv_mul_atTop (a : ℝ) (ha : 0 < a) : Tendsto (fun b : ℝ≥0 => (1 : ℝ) / (a * (b : ℝ))) atTop (𝓝 (0 : ℝ)) := a:ℝha:0 < a⊢ Tendsto (fun b => 1 / (a * ↑b)) atTop (𝓝 0) a:ℝha:0 < ah:Tendsto (fun b => a * ↑b) atTop atTop⊢ Tendsto (fun b => 1 / (a * ↑b)) atTop (𝓝 0) a:ℝha:0 < ah:Tendsto (fun b => a * ↑b) atTop atTop⊢ Tendsto (fun b => (a * ↑b)⁻¹) atTop (𝓝 0) All goals completed! 🐙

Core convergence: as β → ∞, toReal (ofβ β) → 0 in ℝ.

lemma tendsto_toReal_ofβ_atTop : Tendsto (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) atTop (𝓝 (0 : ℝ)) := tendsto_const_inv_mul_atTop kB kB_pos

As β → ∞, T = ofβ β → 0+ in ℝ (within Ioi 0).

lemma tendsto_ofβ_atTop : Tendsto (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) atTop (nhdsWithin 0 (Set.Ioi 0)) := ⊢ Tendsto (fun b => (ofβ b).toReal) atTop (𝓝[>] 0) ⊢ ∀ᶠ (n : ℝ≥0) in atTop, (ofβ n).toReal ∈ Set.Ioi 0 All goals completed! 🐙

Conversion to and from ℝ≥0

Build a Temperature directly from a nonnegative real.

@[simp] def ofNNReal (t : ℝ≥0) : Temperature := ⟨t⟩
@[simp] lemma ofNNReal_val (t : ℝ≥0) : (ofNNReal t).val = t := rfl@[simp] lemma coe_ofNNReal_coe (t : ℝ≥0) : ((ofNNReal t : Temperature) : ℝ≥0) = t := rfl@[simp] lemma coe_ofNNReal_real (t : ℝ≥0) : ((⟨t⟩ : Temperature) : ℝ) = t := rfl

Convenience: build a temperature from a real together with a proof of nonnegativity.

@[simp] noncomputable def ofRealNonneg (t : ℝ) (ht : 0 ≤ t) : Temperature := ofNNReal ⟨t, ht⟩
@[simp] lemma ofRealNonneg_val {t : ℝ} (ht : 0 ≤ t) : (ofRealNonneg t ht).val = ⟨t, ht⟩ := rfl

Calculus relating T and β

Explicit closed-form for Beta_fun_T t when t > 0.

lemma beta_fun_T_formula (t : ℝ) (ht : 0 < t) : betaFromReal t = 1 / (kB * t) := t:ℝht:0 < t⊢ betaFromReal t = 1 / (kB * t) All goals completed! 🐙

On Ioi 0, Beta_fun_T t equals 1 / (kB * t).

lemma beta_fun_T_eq_on_Ioi : EqOn betaFromReal (fun t : ℝ => 1 / (kB * t)) (Set.Ioi 0) := ⊢ EqOn betaFromReal (fun t => 1 / (kB * t)) (Ioi 0) t:ℝht:t ∈ Ioi 0⊢ betaFromReal t = (fun t => 1 / (kB * t)) t All goals completed! 🐙
T:TemperaturehT_pos:0 < T.valhTne:↑T.val ≠ 0hg:HasDerivAt (fun t => kB * t) kB ↑T.valh_deriv:HasDerivAt (fun t => 1 / (kB * t)) (-1 / (kB * ↑T.val ^ 2)) ↑T.val⊢ HasDerivWithinAt betaFromReal (-1 / (kB * ↑T.val ^ 2)) (Ioi 0) ↑T.val All goals completed! 🐙

Chain rule for β(T) : d/dT F(β(T)) = F'(β(T)) * (-1 / (kB * T^2)), within Ioi 0.

F:ℝ → ℝF':ℝT:TemperaturehT_pos:0 < T.valhF_deriv:HasDerivWithinAt F F' (Ioi 0) ↑T.βh_map:MapsTo betaFromReal (Ioi 0) (Ioi 0)h_beta_at_T:betaFromReal ↑T.val = ↑T.βhF_deriv':HasDerivWithinAt F F' (Ioi 0) (betaFromReal ↑T.val)⊢ HasDerivWithinAt (fun t => F (betaFromReal t)) (F' * (-1 / (kB * ↑T.val ^ 2))) (Ioi 0) ↑T.val All goals completed! 🐙