Given a space $X$, I have been thinking about a function $d\colon X \times X \times \mathbb{N} \to \mathbb{R}_{\geq 0}$ (i.e. with values that are nonnegative reals) with the properties below. One may call it a "graded metric". In the concrete examples I have in mind (in quantum computational complexity theory), the integer input ("grading") encodes the amount of available computational resources to "achieve" a measure of closeness, and $d(x,y, k)$ would roughly encode what closeness between two states can be achieved by $k$ computational steps.
The properties are:
- $\forall x,y \in X, k \in \mathbb{N} \colon x=y \rightarrow d(x,y, k) =0$. In contrast to a metric, the other implication doesn't need to hold.
- $\forall x,y,z \in X, k, l\in \mathbb{N} \colon d(x,z, k+l) \leq d(x,y,k) + d(y,z, l)$. This is like a "graded triangle inequality".
- $\forall x,y \in X, k\in \mathbb{N}\colon d(x,y,k) = d(y,x,k)$.
With these properties, the function $d'\colon X\times X \to \mathbb{R}_{\geq 0}, d'(x,y):= \inf_{k \in \mathbb{N}} d(x,y,k)$ is a metric.
In my example, if we can transform a state $x$ to a state $y'$ close to $y$ in $k$ steps, then we can append the $l$ steps that transform $y$ to something close to $z$ to achieve a transformation from $x$ to a state close to $z$. But this operation requires $k+l$ steps in total, leading to property $2$. In some variants of the problem I consider, property $3$ is not correct; without it, we would arrive at an analogue of a quasimetric.
Does this structure, or a similar one, have a name in the literature?
