Temperature

In this module we define the type Temperature, and give basic properties thereof.

def Temperature : Type

The type of temperatures.

Equations

• Temperature = NNReal

noncomputable instance Temperature.instLinearOrder : LinearOrder Temperature

Equations

• Temperature.instLinearOrder = Subtype.instLinearOrder fun (r : ℝ) => 0 ≤ r

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

The underlying real-number associated with the tempature.

Equations

• T.toReal = ↑T

noncomputable instance Temperature.instCoeReal : Coe Temperature ℝ

Equations

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

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

The inverse temperature.

Equations

• T.β = 1 / (↑Constants.kB * T.toReal)