11. The extension by component split
This page proves that a bound T(q)\le C\tau(q) with C\ge0, known for every law q whose support is connected,
holds for every finite law. Here T is the deterministic optimum and \tau the stochastic optimum of section 0 of
the contact page. For a finite law p, let k index the connected components of its support; their
weights \rho_k and normalized laws \bar p_k are defined in Lemma E3.1. The page proves the two inequalities
\sum_k\rho_k\tau(\bar p_k)\le\tau(p) and T(p)\le\sum_k\rho_kT(\bar p_k), and chains them with the bound on each
component. The assembly NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean) proves
T(p)\le(13999/2000)\,\tau(p) for laws with connected support only; NaturalLatents.T_le_c_mul_tau
(NaturalLatents/Main.lean) extends it to every finite law by extension_of_connected (step 9 of the
route).
Each lemma below states its hypotheses, so that it can be read alone. Unless prefixed stoch_to_det, the Lean
declarations named below are in the namespace NaturalLatents.General; the stoch_to_det declarations are in
NaturalLatents/Upstream/, adapted from DLorell/stochtodet. The exceptions
are the declarations called private below (componentIndex, restrict_score_gap, glueLatent_score,
Psi_eq_components, Phi_fiber_decomp, restrictLatent, restrict_score_le, glueLatent and glueLatent_isDet): they
are Lean-private declarations in the namespace stoch_to_det, in the public file NaturalLatents/Upstream/Connected.lean.