Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Mathlib.Analysis.RCLike.BasicUnits 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.
@[expose] public sectionThe choices of translationally-invariant metrics on the temperature-manifold. Such a choice corresponds to a choice of units for temperature.
The underlying scale of the unit.
structure TemperatureUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : TemperatureUnit) : x.val ≠ 0 := x:TemperatureUnit⊢ x.val ≠ 0
All goals completed! 🐙lemma val_pos (x : TemperatureUnit) : 0 < x.val := x.propertyinstance : Inhabited TemperatureUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩Division of TemperatureUnit
lemma div_eq_val (x y : TemperatureUnit) :
x / y = (⟨x.val / y.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt y.val_pos)⟩ : ℝ≥0) := rflx:TemperatureUnity:TemperatureUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0
x:TemperatureUnity:TemperatureUnit⊢ ↑⟨x.val / y.val, ⋯⟩ ≠ 0
All goals completed! 🐙@[simp]
lemma div_pos (x y : TemperatureUnit) : (0 : ℝ≥0) < x/ y := x:TemperatureUnity:TemperatureUnit⊢ 0 < x / y
x:TemperatureUnity:TemperatureUnit⊢ 0 ≤ x / yx:TemperatureUnity:TemperatureUnit⊢ 0 ≠ x / y
x:TemperatureUnity:TemperatureUnit⊢ 0 ≤ x / y All goals completed! 🐙
x:TemperatureUnity:TemperatureUnit⊢ 0 ≠ x / y All goals completed! 🐙@[simp]
lemma div_self (x : TemperatureUnit) :
x / x = (1 : ℝ≥0) := x:TemperatureUnit⊢ x / x = 1
x:TemperatureUnit⊢ ⟨1, ⋯⟩ = 1
All goals completed! 🐙All goals completed! 🐙@[simp]
lemma div_mul_div_coe (x y z : TemperatureUnit) :
(x / y : ℝ) * (y /z : ℝ) = x /z := x:TemperatureUnity:TemperatureUnitz:TemperatureUnit⊢ ↑(x / y) * ↑(y / z) = ↑(x / z)
x:TemperatureUnity:TemperatureUnitz:TemperatureUnit⊢ x.val / y.val * (y.val / z.val) = x.val / z.val
All goals completed! 🐙The scaling of a temperature unit
The scaling of a temperature unit by a positive real.
def scale (r : ℝ) (x : TemperatureUnit) (hr : 0 < r := by norm_num) : TemperatureUnit :=
⟨r * x.val, mul_pos hr x.val_pos⟩@[simp]
lemma scale_div_self (x : TemperatureUnit) (r : ℝ) (hr : 0 < r) :
scale r x hr / x = (⟨r, le_of_lt hr⟩ : ℝ≥0) := x:TemperatureUnitr:ℝhr:0 < r⊢ scale r x hr / x = ⟨r, ⋯⟩
All goals completed! 🐙@[simp]
lemma self_div_scale (x : TemperatureUnit) (r : ℝ) (hr : 0 < r) :
x / scale r x hr = (⟨1/r, _root_.div_nonneg (x:TemperatureUnitr:ℝhr:0 < r⊢ 0 ≤ 1 All goals completed! 🐙) (le_of_lt hr)⟩ : ℝ≥0) := x:TemperatureUnitr:ℝhr:0 < r⊢ x / scale r x hr = ⟨1 / r, ⋯⟩
x:TemperatureUnitr:ℝhr:0 < r⊢ ⟨x.val / (r * x.val), ⋯⟩ = ⟨r⁻¹, ⋯⟩
x:TemperatureUnitr:ℝhr:0 < r⊢ ↑⟨x.val / (r * x.val), ⋯⟩ = ↑⟨r⁻¹, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_one (x : TemperatureUnit) : scale 1 x = x := x:TemperatureUnit⊢ scale 1 x ⋯ = x
All goals completed! 🐙x1:TemperatureUnitx2:TemperatureUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_scale (x : TemperatureUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) :
scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x (mul_pos hr1 hr2) := x:TemperatureUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯
x:TemperatureUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ r1 * (r2 * x.val) = r1 * r2 * x.val
All goals completed! 🐙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.
The definition of a temperature unit of kelvin.
def kelvin : TemperatureUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩