Finite Prime Marginals and Global Support

Abstract

Compatible finite geometric prime-exponent laws coexist with a product law that almost surely has infinitely many active coordinates.

Theorem 1.1 (Finite marginals are compatible while finite global support is null).

$$\begin{array}{r}0<s\le 1,q_{p,s}=p^{-s},{\gamma }_{p,s}=\mathrm{geometricMeasure}\left(1-q_{p,s}\right),{\Gamma }_s=\mathrm{infinitePi}\left({\gamma }_{p,s}\right)\\ \forall S{\subset }_{\mathrm{fin}}\mathbb{P},\mathrm{ProbabilityMeasure}\left(\mathrm{finiteProduct}\left(S,{\gamma }_{p,s}\right)\right)\wedge \mathrm{map}\left(\mathrm{restrict}\left(S\right),{\Gamma }_s\right)=\mathrm{finiteProduct}\left(S,{\gamma }_{p,s}\right)\\ \forall S,e,\mathrm{Pr}\left({\Gamma }_s,\mathrm{Cylinder}\left(S,e\right)\right)=\prod _{p\in S}(1-p^{-s})p^{-s{e}_p}\\ \mathrm{Pr}\left({\Gamma }_s,FiniteSupportProfiles\right)=0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/PrimeProducts/FiniteMarginalGlobalSupportContrast.finite_marginals_and_global_support_contrast (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive real s and prime p, the activation probability is p to the power minus s. The coordinate law is constructed as the zero-start geometric measure with success parameter one minus that activation probability, and the global law is Mathlib’s canonical infinite product of these coordinates.

Every finite coordinate product is a probability measure. Restricting the global product to any finite prime set gives exactly that finite product, and every finite cylinder has the displayed product of geometric singleton masses.

When s is at most one, the prime activation masses have divergent sum. Product-coordinate independence and the second Borel-Cantelli lemma therefore give infinitely many active primes almost surely, so the set of finite-support exponent profiles has measure zero.

References

• Truth anchor: D5/S3/Analytic/PrimeProducts/FiniteMarginalGlobalSupportContrast.finite_marginals_and_global_support_contrast