Multivariate moment determinacy on a compact set

Two finite measures on a compact subset of ι → ℝ (ι finite) that agree on every mixed monomial x ↦ ∏ i, x i ^ n i are equal.

This complements the univariate mechanism in TauCeti/Probability/Moments/Determinacy.lean, which determines a finite measure on ℝ from its polynomial moments under a finite-exponential-moment hypothesis. Here the hypothesis is compact support instead, and the conclusion is multivariate. The two are genuinely different routes: that one is analytic (the moment generating function is analytic on a strip), this one is approximation-theoretic (Stone–Weierstrass).

It supplies the determinacy input consumed by mixedIID_mixingLaw_unique (TauCetiRoadmap/Exchangeability/README.md, Layer 6 — directing measures and de Finetti representation), where the mixed monomials arise as the finite-dimensional moments of a mixture of i.i.d. laws on a compact box.

Main results

• Measure.ext_of_forall_integral_monomial_eq — the compact-subtype form.
• Measure.ext_of_forall_integral_monomial_eq_of_support — the ambient form on ι → ℝ, for measures supported on a common compact set.

Scope

Mixed monomials are finite products of coordinate powers. On a compact subset of a finite real product, their integrals determine a finite measure. The ambient version applies to two finite measures when both are supported on the same compact set.

theorem TauCeti.Measure.ext_of_forall_integral_monomial_eq {ι : Type u_1} {K : Set (ι → ℝ)} [Fintype ι] [CompactSpace ↑K] [MeasurableSpace ↑K] [BorelSpace ↑K] {μ ν : MeasureTheory.Measure ↑K} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hmom : ∀ (n : ι → ℕ), ∫ (x : ↑K), ∏ i : ι, ↑x i ^ n i ∂μ = ∫ (x : ↑K), ∏ i : ι, ↑x i ^ n i ∂ν) : μ = ν

Multivariate moment determinacy on a compact set. Two finite Borel measures on a compact subset K of ι → ℝ that assign the same integral to every mixed monomial x ↦ ∏ i, x i ^ n i are equal.

Compactness is what makes the monomials suffice: it bounds the coordinates, so the polynomial functions are dense in C(K, ℝ) by Stone–Weierstrass. Without it the conclusion fails, as the classical lognormal counterexample on ℝ shows.

theorem TauCeti.Measure.ext_of_forall_integral_monomial_eq_of_support {ι : Type u_1} {K : Set (ι → ℝ)} [Fintype ι] (hK : IsCompact K) {μ ν : MeasureTheory.Measure (ι → ℝ)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : μ Kᶜ = 0) (hν : ν Kᶜ = 0) (hmom : ∀ (n : ι → ℕ), ∫ (x : ι → ℝ), ∏ i : ι, x i ^ n i ∂μ = ∫ (x : ι → ℝ), ∏ i : ι, x i ^ n i ∂ν) : μ = ν

Multivariate moment determinacy, ambient form. Two finite Borel measures on ι → ℝ that are both supported on a common compact set K and assign the same integral to every mixed monomial are equal.

Both support hypotheses are required by this proof, which restricts to the compact subtype: that route establishes only μ.restrict K = ν.restrict K, and each support hypothesis is what identifies one restriction with the original measure.

hν cannot simply be dropped. Classically, a compactly supported finite measure is moment-determinate among all finite measures whose moments exist. But hmom is stated with Bochner integrals, and MeasureTheory.integral_undef makes ∫ f ∂ν = 0 when f is not ν-integrable, so hmom asserts nothing where ν's moments diverge. Taking μ a Dirac mass and ν a Cauchy measure satisfies every hypothesis with hν deleted, since each side of hmom is 0 for n ≠ 0 — on the left because 0 ^ n = 0, on the right because the integral is undefined. So hν is what forces ν's moments to exist at all.

The strengthening that is available replaces hν by moment-integrability of ν, which compact support implies: with genuine moments, a Markov bound on x i ^ (2 * m) confines ν to the same box. That is left to a follow-up; the Layer 6 consumer already has both mixing laws on a common compact box.