- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
The exposure law is generated from an observable characteristic law by one common stochastic map with bounded slack:
with the common carrier \(t\) bi-Lipschitz, \(\ell \, d(x,y)\le \lVert t(x)-t(y)\rVert \le L\, d(x,y)\) for \(0{\lt}\ell \le L\). The constants \(L\), \(\ell \), and the slack radii \(\tau _i\) are maintained modelling restrictions, not quantities the observed distances identify or the empirical design estimates.
If each exposure deviates from a common map value by at most \(\tau _i\), the covariance floor holds with \(LD\) inflated to \(LD+\tau _i+\tau _j\), and exact transmission is the \(\tau =0\) case.
The statement fixes no characteristic distance: \(D\) is an arbitrary nonnegative dissimilarity, and energy distance was only ever one instance. Hosting it under the energy development misread that generality, which is why the declaration now lives in Transmission.Floor and the node here. Contrast ??thm:random-exposure-envelope, which is not distance-agnostic: the sharp envelope needs quadratic transport specifically, because minimising the coupling cost is the same optimisation polarisation turns into an inner product.
At the level of the metric rather than the squared optimized cost, the slack enters additively and no support diameter appears:
This sharper form is what the empirical diagnostic uses.
The upper direction is machine-checked directly at this level: two synchronous-coupling legs bound the slack, one contraction leg carries the transmitted laws, and the \(\mathcal P_2(\mathcal H)\) triangle inequality chains them. The lower direction still needs the reverse Lipschitz half, which supplies injectivity of \(T_\Gamma \) on its image, and remains a prose result. The node keeps notready because it asserts both directions.
Asset \(i\) carries a random loading \(B_i\sim P_i\in \mathcal P_2(\mathcal H)\) in a real Hilbert space \(\mathcal H\), and the common factor process has covariance operator \(\Gamma \). The risk coordinates and factor-weighted second moments are
For a coupling \(\pi \in \Pi (P_i,P_j)\) the systematic covariance is \(\kappa ^\pi _{ij}=\mathbb E_\pi \langle Z_i,Z_j\rangle \), and the factor-weighted quadratic transport cost is
Every object above is now formalized at this level, not only interpreted: risk coordinates as a pushforward under \(\Gamma ^{1/2}\), the second moment and systematic covariance as Bochner integrals, and the transport cost as the infimum defining \(W_2\) on \(\mathcal P_2(\mathcal H)\). The finite instance of ??def:finite-exposure-cloud is the estimator of this object rather than a separate model, and the two agree exactly on finitely supported laws.
One caveat survives and is unchanged: existence of an optimal plan on \(\mathcal P_2(\mathcal H)\) is not proved. It is supplied as a certificate wherever an optimum is needed, so every attainment statement below reads “given such a plan”, never “one exists”.
A finite exposure cloud is a finite support together with nonnegative masses summing to one, and a coupling of two clouds is a nonnegative mass matrix with the two clouds as marginals. Over a coupling this fixes the systematic covariance \(\kappa ^\pi _{ij}\), the transport cost \(C(\pi )\), the second moments \(v_i\), and the barycentre, with no measure-theoretic optimal-transport input. A finite optimal-cost certificate is a separate datum: a coupling together with the assertion that its cost is least in the coupling set.
The Fréchet class of a pair of clouds is the set of systematic covariances \(\kappa ^\pi _{ij}\) attained as \(\pi \) ranges over their couplings. The coupling set is convex and \(\kappa ^\pi _{ij}\) is affine in \(\pi \), so the class is an interval whenever both endpoints are attained.
If standardized total variance decomposes into the certified systematic term and an aggregate residual contribution bounded by \(\delta \geq 0\), then
Multiplication by a nonnegative raw scale gives the corresponding raw-variance inequality. The theorem assumes \(\delta \); it does not estimate it or derive residual orthogonality.
For a finite book with nonnegative weights, the pairwise floors aggregate termwise into a floor on the squared systematic risk. Nonnegativity is a hypothesis, not a convention: signed weights can reverse individual pairwise inequalities and there is no signed-weight counterpart. No weight normalization is assumed, so the screen applies a fortiori to fully-invested long-only books.
??chap:distance-implied carries its own label for this declaration under the distance-implied reading; the two manuscripts consume one theorem.
Against a certified optimal transport cost, \(\operatorname {excess}(\pi )\ge 0\) for every coupling. This is what makes the gap a one-sided moment inequality and hence testable; it is a separate theorem from the identity above, because the identity holds for any reference cost while the sign needs that cost to be the infimum.
For any coupling, \(\kappa ^\pi _{ij}=\kappa ^{\max }_{ij}-\tfrac 12\operatorname {excess}(\pi )\). The checked statement is an identity in the reference cost: it holds for any scalar placed where the optimal cost sits, and therefore asserts nothing about the sign of the excess on its own.
Substituting the metric bracket into the envelope brackets \(\kappa ^{\max }_{ij}\) in observable characteristic distances and the maintained \((L,\ell ,\tau )\). Coverage of this bracket, and the share of unresolved dyads, is the primary reported diagnostic.
Under a positive lower Lipschitz constant and bounded per-endpoint slack, the optimized squared exposure transport cost is at least \(\ell ^{-2}\) times the optimized squared characteristic cost, less a slack term carrying the maintained support diameter.
Under the upper Lipschitz bound and bounded per-endpoint slack, the optimized squared exposure transport cost of two finitely supported clouds is at most \(L^2\) times the optimized squared characteristic cost, plus a slack term carrying the maintained support diameter.
For every coupling \(\pi \) of two finite exposure clouds,
The identity is exact and holds coupling by coupling; no optimality is involved.
The matrix of independently optimal pairwise envelopes \(\left[\kappa ^{\max }_{ij}\right]\) need not be positive semidefinite, because pairwise-optimal couplings may be mutually inconsistent. A globally coherent covariance requires one joint law, as in ??thm:joint-coherence. Stating this boundary is part of the contribution and is not a defect of the envelope.
If \(W_2(\mu ,\nu )\le \delta \) then \(\mathcal E^2(\mu ,\nu )\le 2\delta \); the Wasserstein ball of radius \(\delta \) is therefore contained in the energy-distance ball of radius \(2\delta \). The inclusion is one-directional, and that direction is the pivot’s justification: a \(W_2\) hypothesis is the stronger one, so results proved under it apply to the energy ball, while the converse fails. This node belongs with the trunk rather than with this chapter.
For nonnegative weights and a candidate covariance dominated entrywise by \(U\), the quadratic form is dominated by the form at \(U\); the supremum over the box is therefore attained at the upper corner. No positive-semidefiniteness of \(U\) is required, which is what makes the result usable on a bracket that is not itself a covariance matrix.
Under bi-Lipschitz constants stated in the true, unobserved distance and per-asset embedding radii, the covariance inner product is bracketed by polarization expressions evaluated at the radius-inflated and radius-deflated measured distance. The hypothesis that the bi-Lipschitz relation holds in the unobserved distance is the load-bearing one and is not testable from the measured distances.
Under the same radii, \(\lvert \operatorname {dist}(\mu _i',\mu _j')-\operatorname {dist}(\mu _i,\mu _j)\rvert \le \varepsilon _i+\varepsilon _j\). Additivity on the metric, rather than on the squared quantity, is the same structural fact that makes the metric-level bracket of ??cor:random-w2-metric sharper than its squared counterpart.
Squaring the metric bracket gives an asymmetric interval, with the lower end truncated at zero. The asymmetry is not cosmetic: it is why the squared-cost formalization cannot simply inherit the metric statement.
With a centred isotropic factor and residuals cross-orthogonal to the exposures, the covariance of factor-driven returns equals the systematic covariance of the exposure laws, and the residual cross term vanishes. This is what licenses reading \(\kappa _{ij}\) as a return covariance rather than only as a loading-space inner product; without the orthogonality hypothesis the whole-return claim does not follow.
For mean embeddings perturbed by at most \(\varepsilon _i\) and \(\varepsilon _j\), the inner product moves by at most \(\varepsilon _i\lVert \mu _j\rVert +\varepsilon _j\lVert \mu _i\rVert +\varepsilon _i\varepsilon _j\).
A joint exposure law over all assets reproduces each pairwise systematic covariance on its diagonal coupling, and the induced portfolio quadratic form equals the second moment of the aggregated loading \(B_w=\sum _i w_iB_i\). Coherence is therefore automatic once the object is a single joint law, and the quadratic form is positive semidefinite for that reason alone. This is the honest route around ??prop:pairwise-not-psd.
Under the common non-collapsing carrier, asset-specific synchronous slack, coherent joint-law, marginal, and integrability premises, every normalized long-only portfolio satisfies
The result is a conditional upper bound on systematic variance, not a covariance point estimate or an empirical coverage statement.
Given a finite optimal transport-cost certificate, the ceiling
is the greatest systematic covariance attainable over the coupling set. This is a statement about what the two marginal laws permit; it does not identify the realized covariance, which requires the economic joint law. It is the upper endpoint only; the lower one is ??thm:random-exposure-lower-endpoint, a separate theorem.
For long-only weights the squared systematic risk lies between the quadratic forms of the entrywise lower and upper brackets built from the per-asset radii.