Finite Convex Hulls of Native Declared Probability Laws

Abstract

The native feasible class is generated by finitely many actual probability laws on its original finite carrier, with exact label, source and support constraints.

Theorem 1.1 (Actual probability laws generate the entire feasible class).

$$\begin{array}{r}\exists V\in \mathrm{Finset}\left(\mathrm{ProbabilityMeasure}\left(W\right)\right),V\subseteq F\\ \mathrm{convexHull}\left(\mathrm{massVectorImage}\left(V\right)\right)=\mathrm{massVectorImage}\left(F\right)\\ \forall \theta \in \mathrm{ProbabilityMeasure}\left(W\right),\theta \in F\iff \mathrm{normalizedFiniteMixture}\left(\theta ,V\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/DataProcessing/NativeDeclaredProbabilityPolytope.exists_native_finite_hull (✓ std3). ∎

Source. Repository-derived.

Commentary.

W, Z and U are finite measurable types with measurable singletons. label maps W to Z and source maps W to U. A is any subset of W. Q is an actual probability measure on Z and rho is an actual probability measure on W. No nonempty-feasible-class premise, strict positivity premise or rational-mass premise is imposed.

F consists exactly of those native probability measures theta whose label pushforward is Q, whose full source pushforward equals the source pushforward of this same rho, and whose mass on A is one. The source target is not a separately chosen probability law, and the full source equation is not replaced by marginal equations.

massVector records the real mass of every singleton of W. Its inverse constructs PMF.ofFintype from ENNReal.ofReal of each nonnegative coordinate, then takes the actual induced probability measure. The two maps are inverses. Zero coordinates remain on W; no support subtype or smaller carrier is used.

For every finite indexed family of native laws and nonnegative real coefficients, equality to their ENNReal-weighted measure sum is equivalent to equality to the corresponding real coordinate sum. When the coefficients sum to one, this is the exact finite convex affine correspondence, in both directions.

Under this correspondence, deterministic pushforwards become sums over their full fibers, and mass one on A is equivalent to zero mass at every original symbol outside A. The image of F is exactly the standard simplex sliced by the label, source and outside-support linear equations; both directions of this image equality are supplied.

There exists one finite set V satisfying all three displayed conclusions simultaneously. normalizedFiniteMixture(theta,V) means that there exists a real function a on the entire ProbabilityMeasure W type, nonnegative on V, with sum over V equal to one, such that the underlying measure of theta equals the sum over V of ENNReal.ofReal(a(eta)) times the underlying measure of eta. Coefficients outside V are unrestricted.

The finite-simplex source argument supplies a finite set of coordinate generators. The inverse correspondence reconstructs an actual probability law from each generator. The resulting finite set V lies in F, its mass-coordinate convex hull is exactly the image of F, and a native law belongs to F if and only if it is a nonnegative normalized finite measure sum over that same V.

An empty feasible class is allowed and has an empty generator set. For the inverse-limit application, rho at level l is the actual projection of the one completed world law rho, whose source pushforward is nu. This theorem adds no topological homeomorphism assertion; its conclusion concerns finite probability laws and their affine coordinate representation.

References

• Truth anchor: D5/S3/Estimation/DataProcessing/NativeDeclaredProbabilityPolytope.exists_native_finite_hull
• Dependency: D5/S3/Estimation/DataProcessing/FiniteSimplexFiberPolytope