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.

structure Temperature : Type

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.

• val : NNReal

  The nonnegative real value of the temperature.

instance Temperature.instCoeNNReal : Coe Temperature NNReal

Coercion to ℝ≥0.

Equations

• Temperature.instCoeNNReal = { coe := fun (T : Temperature) => T.val }

noncomputable def Temperature.toReal (T : Temperature) : ℝ

The underlying real-number associated with the temperature.

Equations

• T.toReal = ↑T.val

noncomputable instance Temperature.instCoeReal : Coe Temperature ℝ

Coercion to ℝ.

Equations

• Temperature.instCoeReal = { coe := Temperature.toReal }

instance Temperature.instTopologicalSpace : TopologicalSpace Temperature

Topology on Temperature induced from ℝ≥0.

Equations

• Temperature.instTopologicalSpace = TopologicalSpace.induced (fun (T : Temperature) => T.val) inferInstance

instance Temperature.instZero : Zero Temperature

Equations

• Temperature.instZero = { zero := { val := 0 } }

theorem Temperature.ext {T₁ T₂ : Temperature} (h : T₁.val = T₂.val) : T₁ = T₂

theorem Temperature.ext_iff {T₁ T₂ : Temperature} : T₁ = T₂ ↔ T₁.val = T₂.val

noncomputable def Temperature.β (T : Temperature) : NNReal

The inverse temperature defined as 1/(kB * T) in a given, but arbitrary set of units. This has dimensions equivalent to Energy.

Equations

• T.β = ⟨1 / (Constants.kB * T.toReal), ⋯⟩

noncomputable def Temperature.ofβ (β : NNReal) : Temperature

The temperature associated with a given inverse temperature β.

Equations

• Temperature.ofβ β = { val := ⟨1 / (Constants.kB * ↑β), ⋯⟩ }

theorem Temperature.ofβ_eq : ofβ = fun (β : NNReal) => { val := ⟨1 / (Constants.kB * ↑β), ⋯⟩ }

@[simp]

theorem Temperature.β_ofβ (β' : NNReal) : (ofβ β').β = β'

@[simp]

theorem Temperature.ofβ_β (T : Temperature) : ofβ T.β = T

theorem Temperature.beta_pos (T : Temperature) (hT_pos : 0 < T.val) : 0 < ↑T.β

Positivity of β from positivity of temperature.

Regularity of ofβ

theorem Temperature.ofβ_continuousOn : ContinuousOn ofβ (Set.Ioi 0)

theorem Temperature.ofβ_differentiableOn : DifferentiableOn ℝ (fun (x : ℝ) => ↑(ofβ x.toNNReal).val) (Set.Ioi 0)

Convergence

theorem Temperature.eventually_pos_ofβ : ∀ᶠ (b : NNReal) in Filter.atTop, (ofβ b).toReal > 0

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

theorem Temperature.tendsto_toReal_ofβ_atTop : Filter.Tendsto (fun (b : NNReal) => (ofβ b).toReal) Filter.atTop (nhds 0)

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

theorem Temperature.tendsto_ofβ_atTop : Filter.Tendsto (fun (b : NNReal) => (ofβ b).toReal) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

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

Conversion to and from ℝ≥0

def Temperature.ofNNReal (t : NNReal) : Temperature

Build a Temperature directly from a nonnegative real.

Equations

• Temperature.ofNNReal t = { val := t }

@[simp]

theorem Temperature.ofNNReal_val (t : NNReal) : (ofNNReal t).val = t

@[simp]

theorem Temperature.coe_ofNNReal_coe (t : NNReal) : (ofNNReal t).val = t

@[simp]

theorem Temperature.coe_ofNNReal_real (t : NNReal) : { val := t }.toReal = ↑t

noncomputable def Temperature.ofRealNonneg (t : ℝ) (ht : 0 ≤ t) : Temperature

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

Equations

• Temperature.ofRealNonneg t ht = Temperature.ofNNReal ⟨t, ht⟩

@[simp]

theorem Temperature.ofRealNonneg_val {t : ℝ} (ht : 0 ≤ t) : (ofRealNonneg t ht).val = ⟨t, ht⟩

Calculus relating T and β

noncomputable def Temperature.betaFromReal (t : ℝ) : ℝ

Map a real t to the inverse temperature β corresponding to the temperature Real.toNNReal t (max t 0), returned as a real number.

Equations

• Temperature.betaFromReal t = ↑(Temperature.ofNNReal t.toNNReal).β

theorem Temperature.beta_fun_T_formula (t : ℝ) (ht : 0 < t) : betaFromReal t = 1 / (Constants.kB * t)

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

theorem Temperature.beta_fun_T_eq_on_Ioi : Set.EqOn betaFromReal (fun (t : ℝ) => 1 / (Constants.kB * t)) (Set.Ioi 0)

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

theorem Temperature.deriv_beta_wrt_T (T : Temperature) (hT_pos : 0 < T.val) : HasDerivWithinAt betaFromReal (-1 / (Constants.kB * ↑T.val ^ 2)) (Set.Ioi 0) ↑T.val

theorem Temperature.chain_rule_T_beta {F : ℝ → ℝ} {F' : ℝ} (T : Temperature) (hT_pos : 0 < T.val) (hF_deriv : HasDerivWithinAt F F' (Set.Ioi 0) ↑T.β) : HasDerivWithinAt (fun (t : ℝ) => F (betaFromReal t)) (F' * (-1 / (Constants.kB * ↑T.val ^ 2))) (Set.Ioi 0) ↑T.val

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