PhysLean Documentation

PhysLean.Thermodynamics.Temperature.TemperatureUnits

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 axiomise the existence of a a given temperature unit, and then construct all other temperature units from it. We choose to axiomise the existence of the temperature unit of kelvin, and construct all other temperature units from that.

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
Instances For

    Division of TemperatureUnit #

    @[simp]

    The scaling of a temperature unit #

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

    The scaling of a temperature unit by a positive real.

    Equations
    Instances For
      @[simp]
      theorem TemperatureUnit.scale_div_self (x : TemperatureUnit) (r : ) (hr : 0 < r) :
      scale r x hr / x = r,
      @[simp]
      @[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 must first axiomise the existence of a a given temperature unit, and then construct all other temperature units from it. We choose to axiomise the existence of the temperature unit of kelvin.

      We need an axiom since this relates something to something in the physical world.

      The axiom corresponding to the definition of a temperature unit of kelvin.

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

      Equations
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For