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