Physlib.Thermodynamics.Temperature.Basic

This definition provides a coercion from the type `Temperature` to the set of non-negative real numbers $\mathbb{R}_{\ge 0}$. It allows a temperature $T$ to be treated as its underlying numerical value in $[0, \infty)$, consistent with the convention that absolute zero corresponds to zero.

The function maps a temperature $T$ to its representation as a real number in $\mathbb{R}$.

This definition provides a coercion from the type `Temperature` to the real numbers $\mathbb{R}$. It allows a temperature $T$ to be treated as its numerical representation in $\mathbb{R}$ via the mapping $T \mapsto \text{toReal}(T)$.

The topological space structure on the type `Temperature` is the induced topology from the non-negative real numbers $\mathbb{R}_{\geq 0}$ under the mapping $T \mapsto T.\text{val}$, which assigns to each temperature $T$ its numerical representation in $\mathbb{R}_{\geq 0}$.

The type `Temperature` is equipped with a zero element $0$, which represents the absolute zero of temperature and corresponds to the value $0$ in the underlying numerical representation.

For any two temperatures $T_1, T_2 \in \text{Temperature}$, if their underlying numerical values $T_1.\text{val}$ and $T_2.\text{val}$ in the non-negative real numbers $\mathbb{R}_{\geq 0}$ are equal, then $T_1$ and $T_2$ are equal.

Given a temperature $T$, the inverse temperature $\beta \in \mathbb{R}_{\ge 0}$ is defined by the formula $\beta = \frac{1}{k_B T}$, where $k_B$ is the Boltzmann constant.

Given an inverse temperature $\beta \in \mathbb{R}_{\ge 0}$, this function returns the corresponding temperature $T$ defined as $T = \frac{1}{k_B \beta}$, where $k_B$ is the Boltzmann constant.

The function `ofβ` maps an inverse temperature $\beta \in \mathbb{R}_{\ge 0}$ to a temperature value defined by the expression $\frac{1}{k_B \beta}$, where $k_B$ is the Boltzmann constant.

For any non-negative real number $\beta' \in \mathbb{R}_{\ge 0}$, the inverse temperature $\beta$ associated with the temperature $T$ derived from $\beta'$ (where $T = \text{of}\beta(\beta')$) is equal to $\beta'$. Mathematically, this is expressed as $\beta(\text{of}\beta(\beta')) = \beta'$.

For any temperature $T$, the temperature obtained by converting its inverse temperature $\beta(T)$ back into a temperature value is equal to $T$. Mathematically, this is expressed as $\text{of}\beta(\beta(T)) = T$.

For any temperature $T$, if its value is strictly positive (i.e., $T > 0$), then the corresponding inverse temperature $\beta$ (where $\beta = \frac{1}{k_B T}$) is also strictly positive (i.e., $\beta > 0$).

The function mapping the inverse temperature $\beta \in \mathbb{R}_{\ge 0}$ to the temperature $T$, defined as $T(\beta) = \frac{1}{k_B \beta}$ where $k_B$ is the Boltzmann constant, is continuous on the interval $(0, \infty)$.

The function that maps a real number $x$ to the temperature value $T$ corresponding to an inverse temperature $\beta = x$, defined by $T(x) = \frac{1}{k_B x}$ where $k_B$ is the Boltzmann constant, is differentiable on the interval $(0, \infty)$.

For sufficiently large inverse temperature $\beta \in \mathbb{R}_{\ge 0}$, the corresponding temperature $T(\beta)$, defined as $T(\beta) = \frac{1}{k_B \beta}$ where $k_B$ is the Boltzmann constant, is strictly positive.

Let $T(\beta)$ denote the temperature corresponding to an inverse temperature $\beta \in \mathbb{R}_{\ge 0}$, where $T(\beta) = \frac{1}{k_B \beta}$ and $k_B$ is the Boltzmann constant. As $\beta \to \infty$, the temperature $T(\beta)$ converges to $0$ in $\mathbb{R}$.

Let $T(\beta)$ denote the temperature corresponding to an inverse temperature $\beta \in \mathbb{R}_{\ge 0}$. As $\beta$ tends to infinity, the temperature $T(\beta)$ converges to $0$ from the right in the real numbers $\mathbb{R}$, remaining within the set of positive real numbers $(0, \infty)$ (denoted as $T(\beta) \to 0^+$).

Given a non-negative real number $t \in \mathbb{R}_{\ge 0}$, this function constructs a value of type `Temperature` with magnitude $t$. The resulting `Temperature` is defined in a system of units where $0$ corresponds to absolute zero.

For any non-negative real number $t \in \mathbb{R}_{\ge 0}$, the underlying value of the temperature constructed from $t$ is equal to $t$.

For any non-negative real number $t \in \mathbb{R}_{\ge 0}$, the value of the temperature constructed from $t$, when converted back to a non-negative real number, is equal to $t$.

For any non-negative real number $t \in \mathbb{R}_{\ge 0}$, the real number representation of the temperature constructed from $t$ is equal to $t$.

Given a real number $t \in \mathbb{R}$ and a proof $ht$ that $t \ge 0$, this function constructs a value of type `Temperature` with magnitude $t$. The resulting value represents an absolute temperature in a system of units where $0$ corresponds to absolute zero.

For any real number $t \in \mathbb{R}$ and a proof $h_t$ that $t \ge 0$, the underlying non-negative real value of the temperature constructed from $t$ (denoted by `ofRealNonneg t ht`) is equal to the representation of $t$ as a non-negative real number $\langle t, h_t \rangle \in \mathbb{R}_{\ge 0}$.

Given a real number $t$, the function returns the inverse temperature $\beta$ as a real number. The calculation is performed by first taking the non-negative part of $t$, defined as $T = \max(t, 0)$, and then calculating $\beta = \frac{1}{k_B T}$, where $k_B$ is the Boltzmann constant.

For any real number $t > 0$, the inverse temperature function $\beta(t)$ is given by the closed-form expression $\beta(t) = \frac{1}{k_B t}$, where $k_B$ is the Boltzmann constant.

For any real number $t$ in the interval $(0, \infty)$, the inverse temperature function $\beta(t)$ (defined as `betaFromReal`) is equal to $\frac{1}{k_B t}$, where $k_B$ is the Boltzmann constant.

For a temperature $T$ with a strictly positive value $T > 0$, the inverse temperature function $\beta(t)$ (defined as `betaFromReal`) is differentiable at $t = T$ within the interval $(0, \infty)$. Its derivative at this point is given by $$\frac{d\beta}{dT} = -\frac{1}{k_B T^2}$$ where $k_B$ is the Boltzmann constant.

Let $F: \mathbb{R} \to \mathbb{R}$ be a function and $F' \in \mathbb{R}$. For a temperature $T$ with a strictly positive value $T > 0$, if $F$ is differentiable at $\beta(T)$ within the interval $(0, \infty)$ with derivative $F'$, then the composite function $F(\beta(t))$ is differentiable at $t = T$ within the interval $(0, \infty)$, and its derivative is given by: $$\frac{d}{dT} F(\beta(T)) = F' \cdot \left( -\frac{1}{k_B T^2} \right)$$ where $k_B$ is the Boltzmann constant and $\beta(T) = \frac{1}{k_B T}$ is the inverse temperature.