Weighted coordinate norm and its reduction to a plain coordinate norm

Two total definitions describe weighted coordinate power functionals for real $p$ and real vectors indexed by an arbitrary finite type. In the positive-exponent range, nonnegative weights can be absorbed into a rescaling of the coordinates. The ordinary unweighted functional is a norm in the range $p\ge1$.

weightedNorm attaches a real weight $w_i$ (nonnegative in use) to each coordinate before summing:

reweight rescales each coordinate of $x$ by the corresponding weight raised to the power $1/p$:

By a theorem in the same source module, $\|\operatorname{reweight}(p,w,x)\|_p = \operatorname{weightedNorm}(p,x,w)$ for $p>0$ whenever every $w_i\ge 0$, where $\|\cdot\|_p$ is the finite coordinate power functional (DiagonalConstruction.lpNorm); and $\operatorname{weightedNorm}(p,x,\mathbf{1}) = \|x\|_p$ for the all-ones weight. A further theorem shows that, for fixed $x$ and $p>1$, $w\mapsto\operatorname{weightedNorm}(p,x,w)$ is concave on the nonnegative weights.