Units on Temperature

A unit of temperature corresponds to a choice of translationally-invariant metric on the temperature manifold (to be defined diffeomorphic to ℝ≥0). Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type TemperatureUnit to be equivalent to the positive reals.

On TemperatureUnit there is an instance of division giving a real number, corresponding to the ratio of the two scales of temperature unit.

To define specific temperature units, we first state the existence of a a given temperature unit, and then construct all other temperature units from it. We choose to state the existence of the temperature unit of kelvin, and construct all other temperature units from that.

structure TemperatureUnit : Type

The choices of translationally-invariant metrics on the temperature-manifold. Such a choice corresponds to a choice of units for temperature.

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

theorem TemperatureUnit.val_neq_zero (x : TemperatureUnit) : x.val ≠ 0

theorem TemperatureUnit.val_pos (x : TemperatureUnit) : 0 < x.val

instance TemperatureUnit.instInhabited : Inhabited TemperatureUnit

Equations

• TemperatureUnit.instInhabited = { default := { val := 1, property := TemperatureUnit.instInhabited._proof_1 } }

Division of TemperatureUnit

noncomputable instance TemperatureUnit.instHDivNNReal : HDiv TemperatureUnit TemperatureUnit NNReal

Equations

• TemperatureUnit.instHDivNNReal = { hDiv := fun (x t : TemperatureUnit) => ⟨x.val / t.val, ⋯⟩ }

theorem TemperatureUnit.div_eq_val (x y : TemperatureUnit) : x / y = ⟨x.val / y.val, ⋯⟩

@[simp]

theorem TemperatureUnit.div_neq_zero (x y : TemperatureUnit) : ¬x / y = 0

@[simp]

theorem TemperatureUnit.div_pos (x y : TemperatureUnit) : 0 < x / y

@[simp]

theorem TemperatureUnit.div_self (x : TemperatureUnit) : x / x = 1

theorem TemperatureUnit.div_symm (x y : TemperatureUnit) : x / y = (y / x)⁻¹

@[simp]

theorem TemperatureUnit.div_mul_div_coe (x y z : TemperatureUnit) : ↑(x / y) * ↑(y / z) = ↑(x / z)

The scaling of a temperature unit

def TemperatureUnit.scale (r : ℝ) (x : TemperatureUnit) (hr : 0 < r := by norm_num) : TemperatureUnit

The scaling of a temperature unit by a positive real.

Equations

• TemperatureUnit.scale r x hr = { val := r * x.val, property := ⋯ }

@[simp]

theorem TemperatureUnit.scale_div_self (x : TemperatureUnit) (r : ℝ) (hr : 0 < r) : scale r x hr / x = ⟨r, ⋯⟩

@[simp]

theorem TemperatureUnit.self_div_scale (x : TemperatureUnit) (r : ℝ) (hr : 0 < r) : x / scale r x hr = ⟨1 / r, ⋯⟩

@[simp]

theorem TemperatureUnit.scale_one (x : TemperatureUnit) : scale 1 x ⋯ = x

@[simp]

theorem TemperatureUnit.scale_div_scale (x1 x2 : TemperatureUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 x1 hr1 / scale r2 x2 hr2 = ⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2)

@[simp]

theorem TemperatureUnit.scale_scale (x : TemperatureUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯

Specific choices of temperature units

To define a specific temperature units. We first define the notion of a kelvin to correspond to the temperature unit with underlying value equal to 1. This is really down to a choice in the isomorphism between the set of metrics on the temperature manifold and the positive reals.

Once we have defined kelvin, we can define other temperature units by scaling kelvin.

def TemperatureUnit.kelvin : TemperatureUnit

The definition of a temperature unit of kelvin.

Equations

• TemperatureUnit.kelvin = { val := 1, property := TemperatureUnit.instInhabited._proof_1 }

noncomputable def TemperatureUnit.nanokelvin : TemperatureUnit

The temperature unit of degrees nanokelvin (10^(-9) kelvin).

Equations

• TemperatureUnit.nanokelvin = TemperatureUnit.scale 1e-9 TemperatureUnit.kelvin TemperatureUnit.nanokelvin._proof_1

noncomputable def TemperatureUnit.microkelvin : TemperatureUnit

The temperature unit of degrees microkelvin (10^(-6) kelvin).

Equations

• TemperatureUnit.microkelvin = TemperatureUnit.scale 1e-6 TemperatureUnit.kelvin TemperatureUnit.microkelvin._proof_1

noncomputable def TemperatureUnit.millikelvin : TemperatureUnit

The temperature unit of degrees millikelvin (10^(-3) kelvin).

Equations

• TemperatureUnit.millikelvin = TemperatureUnit.scale 1e-3 TemperatureUnit.kelvin TemperatureUnit.millikelvin._proof_1

noncomputable def TemperatureUnit.absoluteFahrenheit : TemperatureUnit

The temperature unit of degrees fahrenheit ((5/9) of a kelvin). Note, this is fahrenheit starting at 0 absolute temperature.

Equations

• TemperatureUnit.absoluteFahrenheit = TemperatureUnit.scale (5 / 9) TemperatureUnit.kelvin TemperatureUnit.absoluteFahrenheit._proof_3